Mathematical Components

4-colours-cartouche

Summary

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 Odd Order theorem has been completed on September 20th, 2012. Read more here.

Resources

Download sources, browse documentation, subscribe to the users’ mailing list here.

 

  • chercheur2
    Georges Gonthier
    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 ...

2015

Conference papers

titre
Axiomatic constraint systems for proof search modulo theories
auteur
Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Jean-Marc Notin, Assia Mahboubi
article
C. Lutz and S. Ranise. 10th International Symposium on Frontiers of Combining Systems (FroCoS’15), Sep 2015, Wroclaw, Poland. Springer, Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS’15), 9322, 2014, LNAI. <10.1007/978-3-319-24246-0_14>
Accès au bibtex
https://arxiv.org/pdf/1412.6790 BibTex

Reports

titre
A Small Scale Reflection Extension for the Coq system
auteur
Georges Gonthier, Assia Mahboubi, Enrico Tassi
article
[Research Report] RR-6455, Inria Saclay Ile de France. 2015
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00258384/file/main.pdf BibTex

2014

Journal articles

titre
Un ordinateur pour vérifier les preuves mathématiques
auteur
Assia Mahboubi
article
Images des Mathématiques, CNRS, 2014, <http://images.math.cnrs.fr/Un-ordinateur-pour-verifier-les.html>
Accès au bibtex
BibTex

Conference papers

titre
Computer-checked mathematics: a formal proof of the odd order theorem
auteur
Assia Mahboubi
article
The Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2014, Vienna, Austria. <10.1145/2603088.2603090>
Accès au bibtex
BibTex
titre
A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
auteur
Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi
article
ITP – 5th International Conference on Interactive Theorem Proving, 2014, Vienna, Austria. 2014
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00984057/file/main.pdf BibTex

2013

Conference papers

titre
Canonical Structures for the working Coq user
auteur
Assia Mahboubi, Enrico Tassi
article
Sandrine Blazy and Christine Paulin and David Pichardie. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.19-34, 2013, LNCS. <10.1007/978-3-642-39634-2_5>
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00816703/file/main.pdf BibTex
titre
A Machine-Checked Proof of the Odd Order Theorem
auteur
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry
article
Sandrine Blazy and Christine Paulin and David Pichardie. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.163-179, 2013, LNCS. <10.1007/978-3-642-39634-2_14>
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00816699/file/main.pdf BibTex
titre
The Rooster and the Butterflies
auteur
Assia Mahboubi
article
Jacques Carette and David Aspinal and Christopher Lange and Petr Sojka and Wolfgang Windsteiger. CICM 2013 – Conference on Intelligent Computer Mathematics – 2013, Jul 2013, Bath, United Kingdom. Springer, 7961, pp.1-18, 2013, Lecture Notes in Artificial Intelligence. <10.1007/978-3-642-39320-4_1>
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00825074/file/main.pdf BibTex

Books

titre
Homotopy Type Theory: Univalent Foundations of Mathematics
auteur
Peter Aczel, Benedikt Ahrens, Thorsten Altenkirch, Steve Awodey, Bruno Barras, Andrej Bauer, Yves Bertot, Marc Bezem, Thierry Coquand, Eric Finster, Daniel Grayson, Hugo Herbelin, André Joyal, Dan Licata, Peter Lumsdaine, Assia Mahboubi, Per Martin-Löf, Sergey Melikhov, Alvaro Pelayo, Andrew Polonsky, Michael Shulman, Matthieu Sozeau, Bas Spitters, Benno Van den Berg, Vladimir Voevodsky, Michael Warren, Carlo Angiuli, Anthony Bordg, Guillaume Brunerie, Chris Kapulkin, Egbert Rijke, Kristina Sojakova, Jeremy Avigad, Cyril Cohen, Robert Constable, Pierre-Louis Curien, Peter Dybjer, Martín Escardó, Kuen-Bang Hou, Nicola Gambino, Richard Garner, Georges Gonthier, Thomas Hales, Robert Harper, Martin Hofmann, Pieter Hofstra, Joachim Koch, Nicolai Kraus, Nuo Li, Zhaohui Luo, Michael Nahas, Erik Palmgren, Emily Riehl, Dana Scott, Philip Scott, Sergei Soloviev
article
Aucun, pp.448, 2013
Accès au bibtex
BibTex

2012

Journal articles

titre
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
auteur
Cyril Cohen, Assia Mahboubi
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (1:02), pp.1-40. <10.2168/LMCS-8 (1:02) 2012>
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00593738/file/1201.3731.pdf BibTex

Conference papers

titre
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
auteur
François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond
article
Bernhard Gramlich and Dale Miller and Uli Sattler. 6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. Springer, 7364, pp.67-81, 2012, <10.1007/978-3-642-31365-3_8>
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00687640/file/main.pdf BibTex

Reports

titre
Two simulations about DPLL(T)
auteur
Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi
article
2012
Accès au texte intégral et bibtex
http://hal.archives-ouvertes.fr/hal-00690044/file/Main.pdf BibTex

2011

Preprints, Working Papers, …

titre
A Generic Formalised Framework for Reasoning About Weak Memory Models
auteur
Jade Alglave, Assia Mahboubi
article
2011
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00604656/file/itp.pdf BibTex

2010

Journal articles

titre
An introduction to small scale reflection in Coq
auteur
Georges Gonthier, Assia Mahboubi
article
Journal of Formalized Reasoning, ASDD-AlmaDL, 2010, 3 (2), pp.95-152
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00515548/file/main-rr.pdf BibTex

Conference papers

titre
A formal quantifier elimination for algebraically closed fields
auteur
Cyril Cohen, Assia Mahboubi
article
Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. Springer, 6167, pp.189-203, 2010, Computer Science; Intelligent Computer Mathematics. <10.1007/978-3-642-14128-7_17>
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00464237/file/main.pdf BibTex

2009

Conference papers

titre
Packaging Mathematical Structures
auteur
François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau
article
Tobias Nipkow and Christian Urban. Theorem Proving in Higher Order Logics, 2009, Munich, Germany. Springer, 5674, 2009, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00368403/file/main.pdf BibTex

2007

Reports

titre
A Modular Formalisation of Finite Group Theory
auteur
Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
article
[Research Report] RR-6156, INRIA. 2007, pp.17
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00139131/file/RR-6156.pdf BibTex

2015

Communication dans un congrès

titre
Axiomatic constraint systems for proof search modulo theories
auteur
Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Jean-Marc Notin, Assia Mahboubi
article
C. Lutz and S. Ranise. 10th International Symposium on Frontiers of Combining Systems (FroCoS’15), Sep 2015, Wroclaw, Poland. Springer, Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS’15), 9322, 2014, LNAI. <10.1007/978-3-319-24246-0_14>
Accès au bibtex
https://arxiv.org/pdf/1412.6790 BibTex

Rapport

titre
A Small Scale Reflection Extension for the Coq system
auteur
Georges Gonthier, Assia Mahboubi, Enrico Tassi
article
[Research Report] RR-6455, Inria Saclay Ile de France. 2015
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00258384/file/main.pdf BibTex

2014

Article dans des revues

titre
Un ordinateur pour vérifier les preuves mathématiques
auteur
Assia Mahboubi
article
Images des Mathématiques, CNRS, 2014, <http://images.math.cnrs.fr/Un-ordinateur-pour-verifier-les.html>
Accès au bibtex
BibTex

Communication dans un congrès

titre
A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
auteur
Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi
article
ITP – 5th International Conference on Interactive Theorem Proving, 2014, Vienna, Austria. 2014
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00984057/file/main.pdf BibTex
titre
Computer-checked mathematics: a formal proof of the odd order theorem
auteur
Assia Mahboubi
article
The Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2014, Vienna, Austria. <10.1145/2603088.2603090>
Accès au bibtex
BibTex

Rapport

titre
Coq 8.4 Reference Manual
auteur
Pierre Boutillier, Stephane Glondu, Benjamin Grégoire, Hugo Herbelin, Pierre Letouzey, Pierre-Marie Pédrot, Yann Régis-Gianas, Matthieu Sozeau, Arnaud Spiwack, Enrico Tassi
article
[Research Report] Inria. 2014
Accès au bibtex
BibTex

2013

Communication dans un congrès

titre
Canonical Structures for the working Coq user
auteur
Assia Mahboubi, Enrico Tassi
article
Sandrine Blazy and Christine Paulin and David Pichardie. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.19-34, 2013, LNCS. <10.1007/978-3-642-39634-2_5>
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00816703/file/main.pdf BibTex
titre
A Machine-Checked Proof of the Odd Order Theorem
auteur
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry
article
Sandrine Blazy and Christine Paulin and David Pichardie. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.163-179, 2013, LNCS. <10.1007/978-3-642-39634-2_14>
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00816699/file/main.pdf BibTex
titre
Refinements for Free!
auteur
Cyril Cohen, Maxime Dénès, Anders Mörtberg
article
Certified Programs and Proofs, Dec 2013, Melbourne, Australia. pp.147 – 162, 2013, <10.1007/978-3-319-03545-1_10>
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-01113453/file/refinements.pdf BibTex
titre
The Rooster and the Butterflies
auteur
Assia Mahboubi
article
Jacques Carette and David Aspinal and Christopher Lange and Petr Sojka and Wolfgang Windsteiger. CICM 2013 – Conference on Intelligent Computer Mathematics – 2013, Jul 2013, Bath, United Kingdom. Springer, 7961, pp.1-18, 2013, Lecture Notes in Artificial Intelligence. <10.1007/978-3-642-39320-4_1>
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00825074/file/main.pdf BibTex

Ouvrage (y compris édition critique et traduction)

titre
Homotopy Type Theory: Univalent Foundations of Mathematics
auteur
Peter Aczel, Benedikt Ahrens, Thorsten Altenkirch, Steve Awodey, Bruno Barras, Andrej Bauer, Yves Bertot, Marc Bezem, Thierry Coquand, Eric Finster, Daniel Grayson, Hugo Herbelin, André Joyal, Dan Licata, Peter Lumsdaine, Assia Mahboubi, Per Martin-Löf, Sergey Melikhov, Alvaro Pelayo, Andrew Polonsky, Michael Shulman, Matthieu Sozeau, Bas Spitters, Benno Van den Berg, Vladimir Voevodsky, Michael Warren, Carlo Angiuli, Anthony Bordg, Guillaume Brunerie, Chris Kapulkin, Egbert Rijke, Kristina Sojakova, Jeremy Avigad, Cyril Cohen, Robert Constable, Pierre-Louis Curien, Peter Dybjer, Martín Escardó, Kuen-Bang Hou, Nicola Gambino, Richard Garner, Georges Gonthier, Thomas Hales, Robert Harper, Martin Hofmann, Pieter Hofstra, Joachim Koch, Nicolai Kraus, Nuo Li, Zhaohui Luo, Michael Nahas, Erik Palmgren, Emily Riehl, Dana Scott, Philip Scott, Sergei Soloviev
article
Aucun, pp.448, 2013
Accès au bibtex
BibTex

2012

Article dans des revues

titre
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
auteur
Cyril Cohen, Assia Mahboubi
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (1:02), pp.1-40. <10.2168/LMCS-8 (1:02) 2012>
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00593738/file/1201.3731.pdf BibTex

Communication dans un congrès

titre
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
auteur
François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond
article
Bernhard Gramlich and Dale Miller and Uli Sattler. 6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. Springer, 7364, pp.67-81, 2012, <10.1007/978-3-642-31365-3_8>
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00687640/file/main.pdf BibTex
titre
Construction of real algebraic numbers in Coq
auteur
Cyril Cohen
article
Lennart Beringer and Amy Felty. ITP – 3rd International Conference on Interactive Theorem Proving – 2012, Aug 2012, Princeton, United States. Springer, 2012
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00671809/file/main.pdf BibTex
titre
Construction des nombres algébriques réels en Coq
auteur
Cyril Cohen
article
JFLA – Journées Francophones des Langages Applicatifs – 2012, Feb 2012, Carnac, France. 2012
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00665965/file/paper_11.pdf BibTex
titre
A language of patterns for subterm selection
auteur
Georges Gonthier, Enrico Tassi
article
Lennart Beringer, Amy Felty. ITP, Aug 2012, Princeton, United States. Springer, 7406, pp.361-376, 2012, LNCS; Interactive Theorem Proving Interactive Theorem Proving. <10.1007/978-3-642-32347-8_25>
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00652286/file/rew.pdf BibTex

Rapport

titre
Two simulations about DPLL(T)
auteur
Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi
article
2012
Accès au texte intégral et bibtex
http://hal.archives-ouvertes.fr/hal-00690044/file/Main.pdf BibTex

Thèse

titre
Formalized algebraic numbers: construction and first-order theory.
auteur
Cyril Cohen
article
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2012. English
Accès au texte intégral et bibtex
http://pastel.archives-ouvertes.fr/pastel-00780446/file/main.pdf BibTex

2011

Communication dans un congrès

titre
Point-Free, Set-Free Concrete Linear Algebra
auteur
Georges Gonthier
article
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, 6898, pp.103-118, 2011, Lecture Notes in Computer Science; Interactive Theorem Proving – Second International Conference, ITP 2011. <10.1007/978-3-642-22863-6_10>
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00805966/file/main.pdf BibTex
titre
CoqMTU: a higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory
auteur
Bruno Barras, Jean-Pierre Jouannaud, Pierre-Yves Strub, Qian Wang
article
Twenty-Sixth Annual IEEE Symposium on “Logic in Computer Science” – LICS 2011, Jun 2011, Toronto, Canada. 2011
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00583136/file/coq-mtu-lics-2011.pdf BibTex

Thèse

titre
Generic Proof Tools and Finite Group Theory
auteur
François Garillot
article
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2011. English
Accès au texte intégral et bibtex
http://pastel.archives-ouvertes.fr/pastel-00649586/file/manuscript.pdf BibTex

Pré-publication, Document de travail

titre
A Generic Formalised Framework for Reasoning About Weak Memory Models
auteur
Jade Alglave, Assia Mahboubi
article
2011
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00604656/file/itp.pdf BibTex

2010

Article dans des revues

titre
An introduction to small scale reflection in Coq
auteur
Georges Gonthier, Assia Mahboubi
article
Journal of Formalized Reasoning, ASDD-AlmaDL, 2010, 3 (2), pp.95-152
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00515548/file/main-rr.pdf BibTex

Communication dans un congrès

titre
A formal quantifier elimination for algebraically closed fields
auteur
Cyril Cohen, Assia Mahboubi
article
Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. Springer, 6167, pp.189-203, 2010, Computer Science; Intelligent Computer Mathematics. <10.1007/978-3-642-14128-7_17>
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00464237/file/main.pdf BibTex

Pré-publication, Document de travail

titre
Formalizing real analysis for polynomials
auteur
Cyril Cohen
article
2010
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00545778/file/main.pdf BibTex

2009

Article dans des revues

titre
Computing predecessor and successor in rounding to nearest
auteur
Siegfried Rump, Paul Zimmermann, Sylvie Boldo, Guillaume Melquiond
article
BIT Numerical Mathematics, Springer Verlag, 2009, 49 (2), pp.419-431. <10.1007/s10543-009-0218-z>
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00337537/file/RuZiBoMe08.pdf BibTex

Communication dans un congrès

titre
Packaging Mathematical Structures
auteur
François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau
article
Tobias Nipkow and Christian Urban. Theorem Proving in Higher Order Logics, 2009, Munich, Germany. Springer, 5674, 2009, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00368403/file/main.pdf BibTex

Rapport

titre
An Ssreflect Tutorial
auteur
Georges Gonthier, Roux Stéphane Le
article
[Technical Report] RT-0367, INRIA. 2009, pp.33
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00407778/file/RT-367.pdf BibTex

2008

Communication dans un congrès

titre
Proving bounds on real-valued functions with computations
auteur
Guillaume Melquiond
article
Alessandro Armando, Peter Baumgartner, Gilles Dowek. International Joint Conference on Automated Reasoning, IJCAR 2008, Aug 2008, Sydney, Australia. Springer-Verlag, 5195, pp.2–17, 2008, Lecture Notes in Artificial Intelligence. <10.1007/978-3-540-71070-7_2>
Accès au texte intégral et bibtex
http://hal.archives-ouvertes.fr/hal-00180138/file/article.pdf BibTex
titre
Canonical Big Operators
auteur
Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca
article
Theorem Proving in Higher Order Logics, Aug 2008, Montreal, Canada. 5170/2008, 2008, LNCS. <10.1007/978-3-540-71067-7>
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00331193/file/main.pdf BibTex

2007

Rapport

titre
A Modular Formalisation of Finite Group Theory
auteur
Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
article
[Research Report] RR-6156, INRIA. 2007, pp.17
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00139131/file/RR-6156.pdf BibTex

Download sources, browse documentation, subscribe to the users’ mailing list here.