Set-Theory
Set Theory Formalization
A formalization of set theory and its foundational axioms in the Coq proof assistant language
A formalization of the textbook Elements of Set Theory
59 stars
2 watching
4 forks
Language: Coq
last commit: about 3 years ago coqformal-languagesmathset-theorytheorem-proving
Related projects:
| Repository | Description | Stars |
|---|---|---|
| choukh/baby-set-theory | A Coq-based tutorial on set theory and theorem-proving using formalized mathematical proofs | 43 |
 amintimany/categories | An implementation of category theory in the Coq proof assistant. | 93 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 291 |
 geohot/coq-hardy | Formalizing mathematical theorems from Hardy's book in Coq to create a rigorous and reproducible formalization of number theory | 53 |
 jwiegley/category-theory | An axiomatic formalization of category theory in Coq for personal study and practical work | 754 |
 mgrabovsky/fm-notes | A collection of notes and resources on formal methods, type theory, and theorem proving using Coq. | 20 |
 coq-community/dedekind-reals | A formalization of Dedekind reals numbers in the Coq programming language | 43 |
 discus-lang/iron | Formalizations of functional languages with a focus on proof and verification | 141 |
| coq-community/graph-theory | A comprehensive Coq library formalizing various results in graph theory, providing a rigorous foundation for theoretical and applied graph theory research. | 34 |
 hivert/coq-combi | Formalizes algebraic combinatorics in Coq with an emphasis on symmetric functions and their properties. | 1 |
 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 |
 geocoq/geocoq | A formalization of geometry using the Coq proof assistant. | 186 |