proofs
Formal math proofs
A personal repository of formally verified mathematics using the Coq proof assistant
My personal repository of formally verified mathematics.
291 stars
11 watching
12 forks
Language: Coq
last commit: 27 days ago coqformal-verificationinteractive-theorem-provingproof-assistanttype-theory
Related projects:
| Repository | Description | Stars |
|---|---|---|
 choukh/baby-set-theory | A Coq-based tutorial on set theory and theorem-proving using formalized mathematical proofs | 43 |
 math-comp/coq-combi | Formalises algebraic combinatorics in Coq using symmetric functions and polynomials | 36 |
| math-comp/odd-order | Verifies a mathematical theorem in finite group theory | 25 |
 coq-community/coq-100-theorems | Repository tracking famous theorems proved using proof assistants. | 55 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 442 |
| math-comp/abel | Formalization of mathematical theorems about solvability and Galois theory for polynomials | 28 |
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 ilyasergey/pnp | A tutorial project on using Coq to mechanize mathematics with dependent types | 160 |
| choukh/set-theory | A formalization of set theory and its foundational axioms in the Coq proof assistant language | 59 |
 discus-lang/iron | Formalizations of functional languages with a focus on proof and verification | 141 |
 huynhtrankhanh/coqcp | Verifying competitive programming solutions to catch errors and improve rigor through formal mathematical proof | 22 |
| math-comp/math-comp | A comprehensive repository of formalized mathematical theories based on Coq and SSReflect. | 587 |
 coq/platform | A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 188 |
| math-comp/analysis | A comprehensive Coq proof-assistant library for mathematical analysis | 206 |
 yosuke-ito-345/actuary | Formalizes basic actuarial mathematics using Coq | 21 |