MathComp Extra

github.comtool

Extra material for the Mathematical Components library, including the AKS primality test and RSA encryption and decryption.

from

Coq

added

2026-10-10

likes

0

similar

1. ▲
   MathComp School github.com

   tool category #coq link ↗

   Coq sources for lessons and exercises that introduce the SSReflect proof language and the Mathematical Components library.

   
2. ▲
   MathComp Tutorial Materials github.com

   tool category #coq link ↗

   Source code for Mathematical Components tutorials.

3. ▲
   An Introduction to MathComp-Analysis staff.aist.go.jp

   site category #coq link ↗

   Lecture notes on getting started with the Mathematical Components library and using it for classical reasoning and real analysis.

4. ▲
   Mczify github.com

   tool category #coq link ↗

   Library enabling Micromega arithmetic solvers to work when using Mathematical Components number definitions.

   
5. ▲
   Mathematical Components wiki github.com

   site category #coq link ↗
6. ▲
   Analysis github.com

   tool category #coq link ↗

   Library for classical real analysis compatible with Mathematical Components.

Coq › Projects > Libraries: “Extra material for the Mathematical Components library, including the AKS primality test and RSA encryption and decryption.”