Mathematical Components is a repository 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.
Monadic effects and equational reasoning in Rocq
A Rocq formalization of information theory and linear error-correcting codes
The Kalman filter formalized in Rocq/MathComp: discrete Riccati theory (monotonicity, convergence, a unique stabilizing DARE solution), with executable OCaml extraction via CoqEAL.
Extract Rocq definitions to clean Typst markup.
Created by Georges Gonthier
Released 2008
Latest release 2 months ago