Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
-
Updated
Aug 5, 2024 - Coq
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.
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
Docker images of coq-mathcomp [maintainer=@erikmd]
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
A Coq formalization of information theory and linear error-correcting codes
Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]
A proof of Abel-Ruffini theorem.
Graph Theory [maintainers=@chdoc,@damien-pous]
A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
Multinomials for the Mathematical Components library.
Created by Georges Gonthier
Released 2008
Latest release 7 months ago