proofs
Formal math proofs
A personal repository of formally verified mathematics using the Coq proof assistant
My personal repository of formally verified mathematics.
292 stars
11 watching
12 forks
Language: Coq
last commit: about 1 month 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 | Formalizes algebraic combinatorics and symmetric functions in Coq. | 37 |
| math-comp/odd-order | Verifies a mathematical theorem in finite group theory | 27 |
 coq-community/coq-100-theorems | Repository tracking famous theorems proved using proof assistants. | 57 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 444 |
| 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 | 142 |
 huynhtrankhanh/coqcp | Verifying competitive programming solutions to catch errors and improve rigor through formal mathematical proof | 22 |
| math-comp/math-comp | A comprehensive library of formalized mathematical theories | 593 |
 coq/platform | A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 191 |
| math-comp/analysis | A Coq proof-assistant library for real analysis and mathematical structures | 210 |
 yosuke-ito-345/actuary | Formalizes basic actuarial mathematics using Coq | 21 |