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.
Type de document :
Communication dans un congrès
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〉
Liste complète des métadonnées

Littérature citée [36 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00816699
Contributeur : Assia Mahboubi <>
Soumis le : lundi 22 avril 2013 - 17:33:29
Dernière modification le : jeudi 9 février 2017 - 15:47:46
Document(s) archivé(s) le : mardi 23 juillet 2013 - 04:14:29

Fichier

main.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, et al.. A Machine-Checked Proof of the Odd Order Theorem. 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〉. 〈hal-00816699〉

Partager

Métriques

Consultations de la notice

1454

Téléchargements de fichiers

2475