Mathematical Components

Welcome to Mathematical Components' web-page!

Mathematical Components are libraries of formalized mathematics developed using the Coq proof assistant. 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 Coq proof assistant.

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

• The last stable releases of the Mathematical Components library can be downloaded from github.
• Installation instructions.
• Older versions of the Mathematical Components library are also available (historical archives (2008-2014), pre-github archive)

• The source file of each library features a documentation header which describes the concepts and notations introduced in that library.
• The library graph can be explored interactively and the coqdoc presentation of the source files can be browsed online:
  • latest versions:
    • Version 2.3.0 (2024-11-28): library graph, coqdoc presentation
    • Version 2.2.0 (2024-01-17): library graph, coqdoc presentation
    • Version 1.19.0 (2024-01-15): library graph, coqdoc presentation
  • older versions:
    • Version 2.1.0 (2023-10-24): library graph, coqdoc presentation
    • Version 2.0.0 (2023-05-10): library graph, coqdoc presentation
    • Version 1.18.0 (2023-11-01): library graph, coqdoc presentation
    • Version 1.17.0 (2023-05-09): library graph, coqdoc presentation
    • Version 1.16.0 (2023-02-01): library graph, coqdoc presentation
    • Version 2.0+alpha1 (2022-12-05): library graph, coqdoc presentation
    • Version 1.15.0 (2022-06-30): library graph, coqdoc presentation
    • Version 1.14.0 (2022-01-19): library graph, coqdoc presentation
    • Version 1.13.0 (2021-10-28): library graph, coqdoc presentation
    • Version 1.12.0 (2020-11-26): library graph, coqdoc presentation
    • Version 1.11.0 (2020-06-09): library graph, coqdoc presentation
    • Version 1.10.0 (2019-11-29): library graph, coqdoc presentation
• The Ssreflect language comes with a dedicated reference manual, as a chapter of Coq's reference manual.
• A book that introduces the techniques for writing algorithms and proofs and describes the design ideas of the library.

• Chat with us on Coq's Zulip!
• Discuss with us on Coq's Discourse forum!
• Subscribe to the Ssreflect mailing list.
  • 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.