Foundations
Mathematical framework
A mathematical library for a proof assistant that provides the foundation for univalent semantics
Voevodsky's original development of the univalent foundations of mathematics in Coq
53 stars
3 watching
3 forks
Language: Coq
last commit: about 10 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 unimath/foundations | A proof assistant library implementing univalent foundations of mathematics | 240 |
 vafeiadis/hahn | A collection of lemmas and tactics about lists and binary relations for a proof assistant | 30 |
 math-comp/multinomials | A Coq-based library for manipulating monomials and multivariate polynomials over ring structures | 14 |
| unimath/unimath | Formalizes mathematics using the univalent point of view | 961 |
 affeldt-aist/infotheo | A Coq formalization of mathematical foundations for information theory and error-correcting codes | 64 |
 coq-community/gaia | A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics | 28 |
 marshall-lee/software_foundations | A collection of Coq proof solutions to Software Foundations course exercises | 32 |
 choukh/baby-set-theory | A Coq-based tutorial on set theory and theorem-proving using formalized mathematical proofs | 43 |
 zertovitch/mathpaqs | A collection of reusable mathematical components in Ada | 11 |
 adampetcher/fcf | A framework for machine-checked proofs of cryptography in the computational model. | 48 |
| math-comp/mczify | A Coq library that enables the use of Micromega arithmetic solvers for goals stated with Mathematical Components definitions | 23 |
 bmsherman/topology | A programming language and framework for formal topology and probability in Coq. | 32 |
 ilyasergey/pnp | A tutorial project on using Coq to mechanize mathematics with dependent types | 160 |
 dunnl/tealeaves | A framework for abstract syntactical reasoning in Coq. | 23 |
 fibo/algebra | A comprehensive TypeScript library that provides a foundation for abstract algebra and geometric algebra using complex numbers, matrices, and higher-dimensional structures. | 106 |