Mathematical Components

View the Project on GitHub

About

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.

Get the library

Documentation

  • The source file of each library features a documentation header which describes the concepts and notations introduced in that library.
  • The Ssreflect language comes with a dedicated reference manual, as a chapter of Coq's reference manual.
  • A book is in progress, and introduces the techniques for writing algorithms and proofs and describing the design ideas of the library.

More material

Help and contact

Authors and contributors

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