This is a partial list of projects formalizing mathematics in Coq. If your project is missing, please add it.
* The Constructive Coq repository at Nijmegen (C-CoRN) aims at building a computer based library of constructive mathematics. Started in 1999 with a proof of the Fundamental Theorem of Algebra and of the Fundamental Theorem of Calculus, the project covers constructive algebraic structures, metric spaces, effective real analysis.
* The Mathematical Components group develops libraries in group theory and algebra leading to a full formalization of the odd order theorem (Feit-Thompson theorem).
* 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 on his own 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.
* 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.
* At the Mathematical school of the Institute of Advanced Studies, Vladimir Voevodsky is working on the foundations of type theory from a homotopy perspective.
* 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.
See the top 100 mathematical theorems formalized in Coq and the Mathematics category at the Coq user contributions repository.