The Classification of Finite Simple Groups (CFSG) is considered one of the most significant collective achievements in the history of mathematics. The theorem states that every finite simple group—the fundamental building blocks of finite group theory—falls into one of several categories: cyclic groups of prime order, alternating groups, groups of Lie type, or one of 26 'sporadic' groups. Because the original proof was a massive undertaking spanning decades and involving approximately 100 mathematicians across thousands of pages of journal articles, it has long been a candidate for formal verification to ensure its absolute logical integrity.
This image represents the overarching project of formalizing the Classification of Finite Simple Groups using the Lean theorem prover.
Researchers at AxiomMath have now produced a complete formalization of the CFSG in Lean, a functional programming language and interactive theorem prover used to verify mathematical proofs. The project follows the 'first-generation' proof of the CFSG, ensuring that every logical step is checked by Lean's kernel. The formalization is 'sorry-free,' meaning it does not rely on placeholders for unproven steps. The team utilized the TauCeti project's statement of the CFSG as a baseline and built the proof on Mathlib and TauCeti, using standard axioms such as `Classical.choice`, `propext`, and `Quot.sound`.
One of the most significant outcomes of this formalization project was the discovery of a technical error in the existing literature. While verifying the first-generation proof, the team identified a counterexample to a closure assertion used in a published route to the Unbalanced Group Theorem. To resolve this, the team developed an alternative argument for the simple-group case based on Solomon’s 1976 theory of maximal 2-components. This discovery highlights the utility of formal verification: by translating human-written proofs into machine-checkable code, researchers can uncover subtle gaps in complex, multi-author mathematical works that might otherwise remain undetected for years. The project currently consists of over 43 million lines of Lean code and includes an interactive proof map to visualize the dependencies between various papers and books in the corpus.
This image relates to the massive scale of the project and the repository where the formalization is hosted.