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.