Libraries of formalized mathematics

The Mathematical Components library for Coq has its origins in the formal proof of the Four Colour Theorem. Since then it has grown to cover many areas of mathematics and has been used for large scale projects like the formal proof of the Odd Order Theorem.

The library is written using the Ssreflect proof language that is an integral part of the distribution.

The current stable release of the Ssreflect proof language and the Mathematical Components library is version 1.6.1. It supports Coq 8.4pl6 and Coq 8.5pl3 and Coq 8.6.0. It is released under the terms of the CeCILL-B license.

Downloads for version 1.6.1:

- Sources archive
- Windows 32 bits installer for Coq 8.6,
- Windows 64 bits installer for Coq 8.6,

- Sources archive
- Windows 32 bits installer for Coq 8.5, Coq 8.5pl1, Coq 8.5pl2
- Windows 64 bits installer for Coq 8.5, Coq 8.5pl1, Coq 8.5pl2

Older versions of the library are available in the historic archive.

Each source files features a documentation header which describes the concepts and notations introduced in that file. The coqdoc presentation of the source files can be browsed online.

The library graph can be browsed interactively.

The Ssreflect language comes with a dedicated reference manual.

Interested? Subscribe to the ssreflect mailing list and let us know what you are using our libraries for, ask questions, etc. You can also browse the archives of the list or consult the general information page.

The Mathematical Components library and the Ssreflect proof language are developed by the Mathematical Components team, at the Inria -- Microsoft Research Joint Centre.