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, and extended to mathematical analysis.

The libraries are written using the SSReflect proof language, now part of the standard distribution of the Rocq prover. They are built thanks to Hierarchy-Builder, a Rocq plugin.

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