odd-order
Group Theory Theorem Verification
Verifies a mathematical theorem in finite group theory
The formal proof of the Odd Order Theorem
25 stars
16 watching
16 forks
Language: Coq
last commit: 22 days ago
Linked from 2 awesome lists
coqfeit-thompson-theoremmathcompodd-order-theoremssreflect
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 291 |
| 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/fourcolor | A formal proof of a fundamental result in graph theory using the Coq proof assistant | 166 |
 affeldt-aist/infotheo | A Coq formalization of mathematical foundations for information theory and error-correcting codes | 64 |
 geohot/coq-hardy | Formalizing mathematical theorems from Hardy's book in Coq to create a rigorous and reproducible formalization of number theory | 53 |
 thery/mathcomp-extra | A collection of reusable mathematical components and algorithms implemented in Coq | 5 |
 dmxlarchey/kruskal-veldman | A detailed proof of Wim Veldman's tree theorem adaptation in Coq | 0 |
 choukh/baby-set-theory | A Coq-based tutorial on set theory and theorem-proving using formalized mathematical proofs | 43 |
 mgrabovsky/fm-notes | A collection of notes and resources on formal methods, type theory, and theorem proving using Coq. | 20 |
| coq-community/coq-100-theorems | Repository tracking famous theorems proved using proof assistants. | 55 |
| math-comp/math-comp | A comprehensive repository of formalized mathematical theories based on Coq and SSReflect. | 587 |
| choukh/set-theory | A formalization of set theory and its foundational axioms in the Coq proof assistant language | 59 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 442 |
 hivert/coq-combi | Formalizes algebraic combinatorics in Coq with an emphasis on symmetric functions and their properties. | 1 |