Mathematical Components topic
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.
extructures
Finite sets and maps for Coq with extensional equality
Actuary
Formalization of the basic actuarial mathematics using Coq
bits
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
apery
A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
autosubst
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
gaia
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
graph-theory
Graph Theory [maintainers=@chdoc,@damien-pous]
lemma-overloading
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
reglang
Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
Abel
A proof of Abel-Ruffini theorem.