Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata
Contributor : Assia Mahboubi Connect in order to contact the contributor
Submitted on : Wednesday, January 21, 2015 - 8:25:29 PM
Last modification on : Friday, January 21, 2022 - 4:10:01 AM




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⟩



Les métriques sont temporairement indisponibles