Axiom formalises the classification of finite simple groups in Lean
Dozens of AI agents produced about 43.1 million lines of Lean for a proof that runs to about 15,000 pages in more than 500 articles. The work found 34 noteworthy deviations from the published record.
In the Weekly Review of 1 November 2026
Filed under Mathematics
Axiom coordinated AI agents over 24 days to formalise the classification of finite simple groups, one of the longest proofs in mathematics, spread over about 15,000 pages in more than 500 articles. The result is about 43.1 million lines of Lean.
Most discrepancies with the literature were minor, such as typographical errors or dropped hypotheses, but 34 noteworthy deviations needed resolving, the most substantial related to the Unbalanced Group Theorem. The work also produced a new result in group theory, and Axiom is preparing a list of errata in consultation with group theorists.