Assia Mahboubi: Computer-checked mathematics: a formal proof of the odd order theorem. CSL-LICS 2014: 4:1