Here is a Coq mechanized proof of the Odd order theorem, a (huge) step towards the classification: https://github.com/math-comp/odd-order https://github.com/mat

Here is a Coq mechanized proof of the Odd order theorem, a (huge) step towards the classification: https://github.com/math-comp/odd-order https://github.com/math-comp/odd-order The paper is here: https://hal.archives-ouvertes.fr/hal-00816699/ https://hal.archives-ouvertes.fr/hal-00816699/