A Machine-Checked Proof of the Odd Order Theorem.
Georges GonthierAndrea AspertiJeremy AvigadYves BertotCyril CohenFrançois GarillotStéphane Le RouxAssia MahboubiRussell O'ConnorSidi Ould BihaIoana PascaLaurence RideauAlexey SolovyevEnrico TassiLaurent ThéryPublished in: ITP (2013)