Awesome

A formal proof of the Odd Order Theorem

The repository contains a formal verification 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 (a fresh or up to date version of opam 2 is required):

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-odd-order