Reseña: The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups)
Se ha publicado un artículo de razonamiento formalizado en Coq sobre la demostración del teorema de Jordan-Hölder para grupos finitos titulado The rooster and the butterflies.
Su autora es Assia Mahboubi (de Microsoft Research – Inria Joint Centre).
El trabajo se presentará en julio en el CICM 2013 (Conferences on Intelligent Computer Mathematics).
Su resumen es
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.