zbMATH — the first resource for mathematics

The rooster and the butterflies. (English) Zbl 1390.68581
Carette, Jacques (ed.) et al., Intelligent computer mathematics. MKM, Calculemus, DML, and systems and projects 2013, held as part of CICM 2013, Bath, UK, July 8–12, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39319-8/pbk). Lecture Notes in Computer Science 7961. Lecture Notes in Artificial Intelligence, 1-18 (2013).
Summary: This paper describes a machine-checked proof of the Jordan-Hölder theorem for finite groups. This purpose of this description is to discuss the representation of the elementary concepts of finite group theory inside type theory. The design choices underlying these representations were crucial to the successful formalization of a complete proof of the odd order theorem with the Coq system.
For the entire collection see [Zbl 1268.68008].
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
20-04 Software, source code, etc. for problems pertaining to group theory
20D30 Series and lattices of subgroups
Full Text: DOI