Mathematical Components

Welcome to Mathematical Components' web-page!

Mathematical Components are libraries of formalized mathematics developed using the Rocq prover. This project finds its roots in the formal proof of the Four Color Theorem. It has been used for large scale formalization projects, including a formal proof of the Odd Order (Feit-Thompson) Theorem.

The libraries are written using the SSReflect proof language, now part of the standard distribution of the Rocq prover.

This is an open source project, licensed under the CeCILL-B free software license agreement.

• Installation instructions
• The source code of the Mathematical Components library can be downloaded from github.

• A book that introduces the techniques for writing algorithms and proofs and describes the design ideas of the Mathematical Components library.
• The library can be explored interactively and an HTML rendering of the source code can be browsed online:
  • latest versions:
    • Version 2.5.0 (2025-10-13): library graph, coqdoc presentation
    • Version 2.4.0 (2025-04-14): library graph, coqdoc presentation
    • Version 2.3.0 (2024-11-28): library graph, coqdoc presentation
    • Version 2.2.0 (2024-01-17): library graph, coqdoc presentation
  • See this page for older versions.
• The SSReflect proof language comes with a dedicated reference manual, as a chapter of Rocq's reference manual.
• Each file of the source code of the Mathematical Components library features a documentation header which describes the concepts and notations introduced in that file.

• Chat with us on Rocq's Zulip! (in particular via the math-comp channels)
• Discuss with us on Coq's Discourse forum!
• Subscribe to the SSReflect mailing list (low volume).
  • Browse the archives or consult the general information page of the mailing list.

The Mathematical Components library and the SSReflect proof language were initially developed by the Mathematical Components team at the Inria-Microsoft Research Joint Center. Today, the list of members of the Mathematical Components organization is visible here.