coqprime
Prime number verifier
A proof assistant library for prime number certification using elliptic curves and Pocklington certificates
Prime numbers for Coq
37 stars
3 watching
18 forks
Language: Coq
last commit: 2 months ago
Linked from 2 awesome lists
coqelliptic-curvespocklington-certificateprime-numberstheorem-proving
coq-community/awesome-coq
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
 math-comp/coq-combi | Formalizes algebraic combinatorics and symmetric functions in Coq. | 37 |
| thery/mathcomp-extra | A collection of reusable mathematical components and algorithms implemented in Coq | 5 |
 hivert/coq-combi | An algebraic combinatorics library formalized in Coq, providing a comprehensive set of functions and theories for symmetric functions. | 1 |
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 388 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
| thery/flocqlecture | An introductory course on floating-point numbers and formal proof using Coq | 6 |
 mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |
 coq-polyhedra/coq-polyhedra | Formalizes convex polyhedra in Coq using optimization and theorem-proving techniques. | 22 |
| thery/minirubik | Solves the mini Rubik 2x2 using theorem-proving in Coq | 4 |
 uwplse/pumpkin-pi | Automatically discovers and proves relationships between types in Coq to simplify proof development and code reuse. | 49 |
 whonore/coqtail | Enables interactive proof development in Vim similar to other proof assistants. | 274 |
 ilyasergey/pnp | A tutorial project on using Coq to mechanize mathematics with dependent types | 160 |
 huynhtrankhanh/coqcp | Verifying competitive programming solutions to catch errors and improve rigor through formal mathematical proof | 22 |