The Mathematical Components repository
These formal theories cover a wide spectrum of topics, ranging from the formal theory of general purpose data structures like lists, prime numbers or finite graphs, to advanced topics in algebra. The repository includes the foundation of formal theories used in a formal proof of the Four Colour Theorem (Appel - Haken, 1976) and a mechanization of the Odd Order Theorem (Feit - Thompson, 1963), a landmark result of finite group theory, which utilizes the library extensively.
If you already have OPAM installed (a fresh or up to date version of opam 2 is required):
opam repo add coq-released https://coq.inria.fr/opam/released opam install coq-mathcomp-ssreflect
Additional packages go by the name of
coq-mathcomp-field, etc... See INSTALL for detailed
installation instructions in other scenarios.
How to get help
- The website of the MathComp library contains:
- The ssreflect mailing list is the primary venue for help and questions about the library.
- The Mathematical Components Book provides a comprehensive introduction to the library.
- Experienced users hang around at
listening to the