List of Coq Math Projects

This is a partial list of projects formalizing mathematics in Coq. If your project is missing, please add it.

• The Mathematical Components group develops libraries in group theory and algebra leading to a full formalization of the odd order theorem (Feit-Thompson theorem). This group also organized a spring school on the formalization of mathematics in 2012.
• The Constructive Coq repository at Nijmegen (C-CoRN) is a library of constructive mathematics. It includes the Fundamental Theorem of Algebra and the Fundamental Theorem of Calculus, program extraction for real number computation. an abstract model of the real numbers, efficient computation with real numbers and metric spaces inside Coq, an interface to compute with the standard library reals. A simple ODE-solver based on functional analysis. It depends on:
• Math-classes is a library of abstract interfaces for mathematical structures. It is heavily uses type classes.
• The ForMath project gathers researchers from Gothenburg, Nijmegen, Paris-Saclay and La Rioja. It aims at developing libraries of formalized mathematics concerning algebra, linear algebra, real number computation, and algebraic topology.
• Russell O'Connor formalized Gödel's incompleteness theorem in 2003.
• Elements of category theory have been early formalized by Amokrane Saïbi in 1995. Other formalizations are conducted by André Hirschowitz's group at Nice University. Adam Megacz also contributes some libraries. They can also be found in the UniMath and HoTT libraries. Some category theory is also present in Math-classes.
• Formalizations of geometry have been conducted at INRIA Sophia Antipolis by Frédérique Guilhot and Loïc Pottier. Other formalizations are conducted by Julien Narboux, Nicolas Magaud, Pascal Schreck and Jean-François Dufourd at Strasbourg's university, and by Jean Duprat at École Normale Supérieure de Lyon.
• Homotopy type theory is being formalized in the UniMath and HoTT libraries.
• Exact real arithmetic and floating-point arithmetic are investigated by Guillaume Melquiond, Sylvie Boldo, Micaela Mayero, as part of the Gappa, pff and Flocq libraries.
• A formalized proof of the mathematical equivalence between monads and Kleisli triples. The project is here.
• GeoCoq is an attempt to formalize the foundations of geometry in Coq.

See the top 100 mathematical theorems formalized in Coq and the Mathematics category at the Coq user contributions repository.