coq-hardy
Number theory formalism
Formalizing mathematical theorems from Hardy's book in Coq to create a rigorous and reproducible formalization of number theory
Formalizing the Theorems from Hardy's "An Introduction to the Theory of Numbers" in coq
53 stars
5 watching
5 forks
Language: Coq
last commit: over 5 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 geocoq/geocoq | A formalization of geometry using the Coq proof assistant. | 186 |
 choukh/baby-set-theory | A Coq-based tutorial on set theory and theorem-proving using formalized mathematical proofs | 43 |
| choukh/set-theory | A formalization of set theory and its foundational axioms in the Coq proof assistant language | 59 |
 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 |
 math-comp/abel | Formalization of mathematical theorems about solvability and Galois theory for polynomials | 28 |
| math-comp/coq-combi | Formalises algebraic combinatorics in Coq using symmetric functions and polynomials | 36 |
| coq-community/dedekind-reals | A formalization of Dedekind reals numbers in the Coq programming language | 43 |
 jwiegley/category-theory | An axiomatic formalization of category theory in Coq for personal study and practical work | 754 |
 hivert/coq-combi | Formalizes algebraic combinatorics in Coq with an emphasis on symmetric functions and their properties. | 1 |
| coq-community/hydra-battles | Investigating various aspects of discrete mathematics and formal proofs in Coq, including ordinal numbers and computability theory. | 68 |
 mgrabovsky/fm-notes | A collection of notes and resources on formal methods, type theory, and theorem proving using Coq. | 20 |
| coq-community/gaia | A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics | 28 |
 unimath/unimath | Formalizes mathematics using the univalent point of view | 961 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
| coq-community/fourcolor | A formal proof of a fundamental result in graph theory using the Coq proof assistant | 166 |