A machine-checked proof of the odd order theorem

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

doi:10.1007/978-3-642-39634-2_14

A machine-checked proof of the odd order theorem

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

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

Abstract

This paper reports on a six-year collaborative effort that culminated in a complete formalization of a proof of the Feit-Thompson Odd Order Theorem in the Coq proof assistant. The formalized proof is constructive, and relies on nothing but the axioms and rules of the foundational framework implemented by Coq. To support the formalization, we developed a comprehensive set of reusable libraries of formalized mathematics, including results in finite group theory, linear algebra, Galois theory, and the theories of the real and complex algebraic numbers. © 2013 Springer-Verlag.

Original language	English
Title of host publication	Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings
Pages	163-179
DOIs	https://doi.org/10.1007/978-3-642-39634-2_14
Publication status	Published - 2013
Externally published	Yes
Event	4th International Conference on Interactive Theorem Proving, ITP 2013 - , France Duration: 22 Jul 2013 → 26 Jul 2013

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	4th International Conference on Interactive Theorem Proving, ITP 2013
Country/Territory	France
Period	22/07/13 → 26/07/13

Access to Document

10.1007/978-3-642-39634-2_14

Persistent URL (handle)

Persistent link

Cite this

Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O'Connor, R., Ould Biha, S., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., & Théry, L. (2013). A machine-checked proof of the odd order theorem. In Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings (pp. 163-179). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-39634-2_14

@inproceedings{674e787d177441878046160769328b2f,

title = "A machine-checked proof of the odd order theorem",

abstract = "This paper reports on a six-year collaborative effort that culminated in a complete formalization of a proof of the Feit-Thompson Odd Order Theorem in the Coq proof assistant. The formalized proof is constructive, and relies on nothing but the axioms and rules of the foundational framework implemented by Coq. To support the formalization, we developed a comprehensive set of reusable libraries of formalized mathematics, including results in finite group theory, linear algebra, Galois theory, and the theories of the real and complex algebraic numbers. {\textcopyright} 2013 Springer-Verlag.",

author = "Georges Gonthier and Andrea Asperti and Jeremy Avigad and Yves Bertot and Cyril Cohen and Fran{\c c}ois Garillot and {Le Roux}, St{\'e}phane and Assia Mahboubi and Russell O'Connor and {Ould Biha}, Sidi and Ioana Pasca and Laurence Rideau and Alexey Solovyev and Enrico Tassi and Laurent Th{\'e}ry",

year = "2013",

doi = "10.1007/978-3-642-39634-2_14",

language = "English",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "163--179",

booktitle = "Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings",

note = "4th International Conference on Interactive Theorem Proving, ITP 2013 ; Conference date: 22-07-2013 Through 26-07-2013",

}

Gonthier, G, Asperti, A, Avigad, J, Bertot, Y, Cohen, C, Garillot, F, Le Roux, S, Mahboubi, A, O'Connor, R, Ould Biha, S, Pasca, I, Rideau, L, Solovyev, A, Tassi, E & Théry, L 2013, A machine-checked proof of the odd order theorem. in Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 163-179, 4th International Conference on Interactive Theorem Proving, ITP 2013, France, 22/07/13. https://doi.org/10.1007/978-3-642-39634-2_14

A machine-checked proof of the odd order theorem. / Gonthier, Georges; Asperti, Andrea; Avigad, Jeremy et al.
Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings. 2013. p. 163-179 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A machine-checked proof of the odd order theorem

AU - Gonthier, Georges

AU - Asperti, Andrea

AU - Avigad, Jeremy

AU - Bertot, Yves

AU - Cohen, Cyril

AU - Garillot, François

AU - Le Roux, Stéphane

AU - Mahboubi, Assia

AU - O'Connor, Russell

AU - Ould Biha, Sidi

AU - Pasca, Ioana

AU - Rideau, Laurence

AU - Solovyev, Alexey

AU - Tassi, Enrico

AU - Théry, Laurent

PY - 2013

Y1 - 2013

N2 - This paper reports on a six-year collaborative effort that culminated in a complete formalization of a proof of the Feit-Thompson Odd Order Theorem in the Coq proof assistant. The formalized proof is constructive, and relies on nothing but the axioms and rules of the foundational framework implemented by Coq. To support the formalization, we developed a comprehensive set of reusable libraries of formalized mathematics, including results in finite group theory, linear algebra, Galois theory, and the theories of the real and complex algebraic numbers. © 2013 Springer-Verlag.

AB - This paper reports on a six-year collaborative effort that culminated in a complete formalization of a proof of the Feit-Thompson Odd Order Theorem in the Coq proof assistant. The formalized proof is constructive, and relies on nothing but the axioms and rules of the foundational framework implemented by Coq. To support the formalization, we developed a comprehensive set of reusable libraries of formalized mathematics, including results in finite group theory, linear algebra, Galois theory, and the theories of the real and complex algebraic numbers. © 2013 Springer-Verlag.

UR - http://www.scopus.com/inward/record.url?scp=84882793903&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-39634-2_14

DO - 10.1007/978-3-642-39634-2_14

M3 - Conference contribution

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 163

EP - 179

BT - Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings

T2 - 4th International Conference on Interactive Theorem Proving, ITP 2013

Y2 - 22 July 2013 through 26 July 2013

ER -

Gonthier G, Asperti A, Avigad J, Bertot Y, Cohen C, Garillot F et al. A machine-checked proof of the odd order theorem. In Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings. 2013. p. 163-179. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-39634-2_14

A machine-checked proof of the odd order theorem

Abstract

Publication series

Conference

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this