iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://hal.inria.fr/hal-00816699
A Machine-Checked Proof of the Odd Order Theorem - Inria - Institut national de recherche en sciences et technologies du numérique
Communication Dans Un Congrès Année : 2013

A Machine-Checked Proof of the Odd Order Theorem

Stéphane Le Roux

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (230.69 Ko) Télécharger le fichier
Origine Fichiers éditeurs autorisés sur une archive ouverte
Loading...

Dates et versions

hal-00816699 , version 1 (22-04-2013)

Identifiants

Citer

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⟩

Collections

INRIA INRIA2
8672 Consultations
6610 Téléchargements

Altmetric

Partager

More