The formal proof of the Odd Order Theorem
-
Updated
Jul 24, 2026 - Rocq Prover
#
odd-order-theorem
Here are 3 public repositories matching this topic...
The Feit–Thompson odd order theorem in Lean 4, with the finite group theory library it required — Hall, Fitting, Frobenius groups, transfer, ZJ, Dade isometry, coherence
-
Updated
Aug 7, 2026 - Lean
Self-contained lean-eval submission of the Feit–Thompson theorem, extracted from yawara/odd-order
-
Updated
Jul 16, 2026 - Lean
Improve this page
Add a description, image, and links to the odd-order-theorem topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the odd-order-theorem topic, visit your repo's landing page and select "manage topics."