Mathematical Components

View the Project on GitHub


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


Mathematical Components book

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 Center. Today, the list of members of the Mathematical Components organization is visible here.