Axiom formalizes the classification of finite simple groups in Lean

Startup Axiom announced a complete formalization, in the Lean proof assistant, of the Classification of Finite Simple Groups, a result mathematicians call the periodic table of symmetry. The original proof spans roughly 15,000 pages and was built by more than 100 mathematicians across generations, showing that every finite simple group is cyclic of prime order, alternating, of Lie type, or one of 26 sporadic groups.

Axiom's project site puts the formalization at 43.1 million lines of Lean code, 2.05 million declarations, 100 milestones, and 715 source papers and books referenced, with every logical step checked by Lean's kernel. The team says that while formalizing the first-generation proof, they found an issue in a published argument used for the Unbalanced Group Theorem, a key piece of the overall classification, and had to build an alternative route based on Solomon's 1976 theory of maximal 2-components. They describe this as a new mathematical result that came directly out of the formalization work, and say they are compiling further errata found in the literature to publish.

The project lists a large group of mathematical and engineering contributors, with Letong Hong credited as principal investigator. Axiom's work is available through its interactive proof map site and a GitHub repository.

Why it matters

Full machine verification of one of the largest proofs in mathematics is a strong signal that AI-assisted formalization can both check and improve long-standing mathematical literature.

Source: Axiom on X