A Modular Formalisation of Finite Group Theory - Gonthier, Georges; Mahboubi, Assia; Rideau, Laurence; Tassi, Enrico; Théry, Laurent (Springer-Verlag, 2007)
In this paper, we present a formalisation of elementary group theory done in Coq. This work is the first milestone of a long-term effort to formalise the Feit-Thompson theorem. As our further developments will heavily rely on this initial base, we took special care to articulate it in the most compositional way.