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 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.