The classification of finite simple groups is formalised in Lean

The classification states that every finite simple group is cyclic of prime order, alternating, of Lie type, or one of 26 sporadic groups. Its first-generation proof runs to roughly 15,000 pages across more than 500 articles by about 100 mathematicians, and was completed only in 2004 with Aschbacher and Smith’s treatment of quasithin groups. Axiom announced on 26 October that it had formalised this proof in Lean, with every logical step checked by Lean’s kernel.

The company says engineers and mathematicians directed swarms of dozens of AI agents over 24 days, producing about 43.1 million lines of Lean and 2.05 million declarations. The work drew on 715 papers and books. Most problems found in the literature were minor, such as typographical errors, errors in tables and dropped hypotheses, but Axiom counted 34 noteworthy deviations from the published record.

The most substantial concerned the Unbalanced Group Theorem: the team found counterexamples to a closure assertion used in one published route and gives an alternative argument for the simple-group case in an accompanying 35-page paper. Axiom says it will publish the errata in consultation with group theorists. The Feit–Thompson theorem, one step of the classification, was formalised in Coq in 2012 after a six-year effort.