Axiom says its AI system formalized the 15,000-page classification of finite simple groups in Lean in 24 days
The company says the effort produced about 43.1 million lines of Lean code and found a significant gap in one part of the original proof.
Axiom Math announced on October 26 that its AxiomProver system has completed a computer-checkable formal version of the Classification of Finite Simple Groups. TokenPost reports that the company describes it as the first complete formalization of the result. The original proof runs to about 15,000 pages, draws on more than 500 papers, and was built over several decades by more than 100 mathematicians. Axiom says the project took 24 days and produced about 43.1 million lines of code in Lean, a language that expresses mathematical statements and proofs so that software can check whether each deduction follows. The company also says the work exposed a significant gap in the proof of the Unbalanced Group Theorem. The classification states that every finite simple group falls into one of four categories: cyclic groups of prime order, alternating groups, groups from 16 families of Lie type, or 26 sporadic groups. These groups are the building blocks into which all finite groups can be broken down. AxiomProver uses multiple AI agents. Mathematicians have long seen this theorem as one of the hardest results to verify because of its size. If the claim holds up under outside review, it would show that AI-driven formalization can work at a scale that had been out of reach, and that it can surface real gaps in accepted mathematics.