The object of this project is to demonstrate that formalized mathematical theories can, like modern software, be built out of components. By components we mean modules that comprise both the static (objects and facts) and dynamic (proof and computation methods) contents of theories. We propose to develop a general platform for mathematical components, based on the Coq “Ssreflect” extension that was used to carry out the formalization of the Four Colour Theorem. We would validate the platform on two significant developments: a theory of efficient arithmetic, and the proof of the Odd Order theorem. The former could be used in the resolution of several outstanding computer proof challenges, among them the Kepler Conjecture, and the latter could become the first step in a new major challenge: the classification of finite simple groups.
Current state of the project
The formal proof of the Feit-Thompson theorem has been completed on September 20, 2012.
Georges Gonthier graduated from Ecole Normale Supérieure in Paris, he received his PhD from the University of Paris 11, worked at AT&T Bell laboratories for 2 years and at INRIA for 13 years. He is presently a senior researcher at Microsoft ...
Lennart Beringer, Amy Felty. ITP, Aug 2012, Princeton, United States. Springer, Interactive Theorem Proving Interactive Theorem Proving, 7406, pp. 361-376, LNCS
Bernhard Gramlich and Dale Miller and Uli Sattler. 6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. Springer, Automated Reasoning, 7364, pp. 67-81, Lecture Notes in Computer Science
Marko C. J. D. van Eekelen and Herman Geuvers and Julien Schmaltz and Freek Wiedijk. Interactive Theorem Proving – ITP 2011, Aug 2011, Berg en Dal, Netherlands. Springer, Interactive Theorem Proving – Second International Conference, ITP 2011, 6898, pp. 103-118, Lecture Notes in Computer Science
Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. Springer, Intelligent Computer Mathematics, 6167, pp. 189-203, Computer Science
Alessandro Armando, Peter Baumgartner, Gilles Dowek. International Joint Conference on Automated Reasoning, IJCAR 2008, Aug 2008, Sydney, Australia. Springer-Verlag, 5195, pp. 2-17, Lecture Notes in Artificial Intelligence
We are pleased to announce the latest full release of the Ssreflect extension library for the Coq proof assistant, version 8.3pl4 and 8.4. Distributed under the CeCILL B license (the French equivalent of the BSD license)
Ssreflect version 1.2 is distributed under either one (your choice) of the CeCILLBor CeCILL 2 license (the French equivalents of the BSD and GNU/GPL license, respectively): Download
Ssreflect version 1.1, for the Coq proof assistant, version 8.1. Distributed under the CeCILL B license (the French equivalent of the BSD license):Download
Coq sources for the proof of the Four Color Theorem, for the Coq proof assistant, version 8.0. Distributed as an MSR distribution: Download
; François Garillot 
