Computer-checked mathematics: a formal proof of the odd order theorem

Abstract : The Odd Order Theorem is a landmark result in finite group theory, due to W. Feit and J. G. Thompson [1], which states that every finite group of odd order is solvable. It is famous for its crucial role in the classification of finite simple groups, for the novel methods introduced by its original proof but also for the striking contrast between the simplicity of its statement and the unusual length and complexity of its proof. After a six year collaborative effort, we managed to formalize and machine-check a complete proof of this theorem [2] using the Coq proof assistant [3]. The resulting collection of libraries of formalized mathematics covers a wide variety of topics, mostly in algebra, as this proof relies on a sophisticated combination of local analysis and character theory. In this tutorial we comment on the role played by the different features of the proof assistant, from the meta-theory of its underlying logic to the implementation of its various components. We will also discuss some issues raised by the translation of mathematical textbooks into formal libraries and the perspectives it opens on the use of a computer to do mathematics.
Type de document :
Communication dans un congrès
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〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01107941
Contributeur : Assia Mahboubi <>
Soumis le : mercredi 21 janvier 2015 - 20:25:29
Dernière modification le : jeudi 9 février 2017 - 15:48:31

Identifiants

Collections

Citation

Assia Mahboubi. Computer-checked mathematics: a formal proof of the odd order theorem. 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〉. 〈hal-01107941〉

Partager

Métriques

Consultations de la notice

246