The repository contains a mechanization of the Odd Order Theorem (Feit - Thompson, 1963), a landmark result of finite group theory.
The formal proof is based on the Mathematical Components library for the Coq proof assistant.
If you already have OPAM installed:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-odd_order