Widely considered the longest proof in mathematics, now machine-checked: dozens of AI agents wrote 43.1 million lines of Lean in 24 days
Synopsis
The classification of finite simple groups — the longest mathematical proof humans have written — now exists as a complete, computer-checked proof. That "enormous theorem" had been spread across more than 500 articles and roughly 15,000 pages, written over decades by about 100 mathematicians. Engineers and mathematicians at Axiom Math directed swarms of dozens of AI agents for 24 days, producing about 43.1 million lines of Lean code, and recorded 34 noteworthy deviations from the published record, the largest of which concerned the Unbalanced Group Theorem; the process also yielded a new theorem in group theory.
Interpretation
The classification of finite simple groups, the list of the basic atoms of finite symmetry, now has a complete proof that a computer can check step by step. The argument known as the enormous theorem was spread over more than 500 articles and roughly 15,000 pages by about 100 mathematicians, and the 1983 announcement of completion did not hold, because one quasithin case rested on an unfinished manuscript that stayed open until Aschbacher and Smith published a 1,221-page treatment in 2004. What makes the check believable is a concrete counterexample thrown up during translation: formalization recorded 34 noteworthy deviations, the largest around the Unbalanced Group Theorem, where Walter's 1986 argument assumed an operation kept the relevant simple groups inside a specified family, agents found a group explicitly excluded from that family, and the project supplied a replacement argument resting on Solomon's 1976 theory of maximal 2-components, written up as a new theorem in group theory.
The hard part is not writing any single long argument but making the definitions, hypotheses and conclusions written by dozens of agents in parallel fit together. A proof map assembled from the published literature split the work into 108 milestones and about 380 smaller tasks, agents claimed milestones through GitHub issues and reported in Slack, and the Lean proof assistant recorded each deduction in a form that could be checked line by line, so a gap could not be stepped over. As the shared repository grew, agents wrote proofs faster than Lean could recheck them, so engineers distributed cached build results across machines for parallel checks and moved expensive finite computations into separately checkable certificates, making verification orders of magnitude faster.
Perspective
The formalization covers the first generation proof, so its scope is fixed to the arguments used there; the second generation multi-volume proof is still in progress and is now expected to run to at least twelve volumes. It is meant for readers and group theorists who want to trace which results a step depends on and what its hypotheses say, and the release makes the final theorem and the checking instructions public while the project continues curating errata with an advisory board including Richard Lyons and Ronald Solomon.
Lean checks the deductions of a formal statement; whether that statement really expresses the intended classification still needs a human reading of the statement and its definitions. Whether a formal development reproduces each step of a particular historical argument is a separate question, and the Unbalanced Group Theorem took a different route. The errata list and its corrections will keep being curated.