A machine-checked proof of the odd order theorem. (English) Zbl 1317.68211

Gonthier, Georges; Asperti, Andrea; Avigad, Jeremy; Bertot, Yves; Cohen, Cyril; Garillot, François; Le Roux, Stéphane; Mahboubi, Assia; O’Connor, Russell; Ould Biha, Sidi; Pasca, Ioana; Rideau, Laurence; Solovyev, Alexey; Tassi, Enrico; Théry, Laurent

Blazy, Sandrine (ed.) et al., Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22–26, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39633-5/pbk). Lecture Notes in Computer Science 7998, 163-179 (2013).

Summary: This paper reports on a six-year collaborative effort that culminated 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.
For the entire collection see [Zbl 1268.68006].

MSC:

68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35	Mechanization of proofs and logical operations
20-04	Software, source code, etc. for problems pertaining to group theory
20D10	Finite solvable groups, theory of formations, Schunck classes, Fitting classes, \(\pi\)-length, ranks

Keywords:

Feit-Thompson odd order theorem

Software:

Coq/SSReflect; Coq