Axiom’s AI agents formalise the classification of finite simple groups in Lean in 24 days
See how this story connectsAxiom Math released a complete Lean formalisation of the Classification of Finite Simple Groups on 26 October 2026, formalising the first-generation proof, which runs to roughly 15,000 pages in more than 500 articles by about 100 mathematicians. Over 24 days, from 2 October, Axiom’s engineers and mathematicians directed swarms of dozens of AI agents, which used a changing mix of models. The agents produced about 43.1 million lines of Lean and 2.05 million declarations across 108 milestones. The work found 34 noteworthy deviations from the published record, the largest in an argument for the Unbalanced Group Theorem, and produced a new group theory result, written up in a 35-page paper. Axiom says it will publish the errata with group theorists.
Why it matters
The proof usually called the longest in mathematics now has every step checked by Lean’s kernel, and group theorists will get a list of errors and gaps in the papers it rests on.
- When
- 26 Oct 2026
- ID
WTA-N-2026-0462- Where
- United States
- Who
- Axiom Math
- Topics
- Mathematics, AI agents, Research
Summary written with AI by wheresthe.ai, from Axiom. Checked against the source on 28 Oct 2026.
Source copy: saved on 28 Oct 2026 to check this story and not republished, because the text belongs to its publisher. Also held by the Internet Archive.
Cite this story
WTA-N-2026-0462: “Axiom’s AI agents formalise the classification of finite simple groups in Lean in 24 days.” wheresthe.ai, 26 Oct 2026. https://wheresthe.ai/d/us-axiom-formalizes-classification-of-finite-simple-groups-in-lean-2026-10/ (source: Axiom).
Spotted an error? Email [email protected].