The Mathematical Components Library is an extensive and coherent repository of formalized mathematical theories. It is based on the Coq/Rocq proof assistant, powered with the SSReflect language.
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-algebra,
coq-mathcomp-field, etc... See INSTALL for detailed
installation instructions in other scenarios.
- The website of the MathComp library
contains:
- links to the HTML documentation of the last version as well as the documentation of previous versions,
- a list of tutorials.
- The Mathematical Components Book provides a comprehensive introduction to the library.
- Experienced users hang around at
StackOverflow
listening to the
ssreflectandcoqtags. - The primary venue for help and questions about the library nowadays is Zulip.
- Developers and users can also be reached via the ssreflect mailing list (low volume).
- The MathComp library has been regularly released since 2008. Recently, we have been releasing a new version twice a year, in line with the released of the Coq/Rocq proof assistant.
- Changes are documented systematically in CHANGELOG.md and CHANGELOG_UNRELEASED.md.
- We use deprecation warnings to help transitioning to new versions (see CONTRIBUTING.md for details about the deprecation policy).
A collection of papers using the Mathematical Components library