A Machine-Checked Proof of the Odd Order Theorem

Abstract : This paper reports on a six-year collaborative effort that cul- minated 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.
Complete list of metadatas

Cited literature [36 references]  Display  Hide  Download

https://hal.inria.fr/hal-00816699
Contributor : Assia Mahboubi <>
Submitted on : Monday, April 22, 2013 - 5:33:29 PM
Last modification on : Wednesday, September 12, 2018 - 1:16:38 AM
Long-term archiving on : Tuesday, July 23, 2013 - 4:14:29 AM

File

main.pdf
Publisher files allowed on an open archive

Identifiers

Collections

Citation

Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, et al.. A Machine-Checked Proof of the Odd Order Theorem. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.163-179, ⟨10.1007/978-3-642-39634-2_14⟩. ⟨hal-00816699⟩

Share

Metrics

Record views

4246

Files downloads

4390