AI agents formalize 15,000-page math proof in 24 days, find 34 errors

Key Points

1. Axiom Math says AI agent swarms formalized the classification of finite simple groups in Lean.
2. The original proof spans roughly 15,000 pages across 500-plus papers by about 100 mathematicians.
3. Machine-checking humanity's largest proof surfaced 34 deviations human referees had let stand for decades.

The latest:

Roughly 43.1 million lines of Lean code, produced in 24 days by swarms of dozens of AI agents, now carry a complete machine-checked formalization of the classification of finite simple groups, Axiom Math said in an October 26, 2026 research post. The company called the classification the periodic table of symmetry and the largest mathematical proof in human history. Lean verified every dependency automatically.

Details:

• The scale: Axiom said the original argument runs about 15,000 pages across more than 500 papers written by roughly 100 mathematicians over generations. The formalization absorbed about 1.2 million lines from the Qiuzhen-CFSG project plus Mathlib, organized into 108 milestones and some 380 smaller tasks.
• The timeline: According to Axiom, a dedicated Slack channel opened October 1, 2026, and the first agent swarm launched the next day. On October 10 the agents proved the Monster group is simple, marked by a Slack message reading “WE PROVED MONSTER IS SIMPLE.” Coordination ran through Slack, GitHub issues and a proof map.
• The system: The work was run by AxiomProver, with agents using a shifting mix of models and orchestration tools under the direction of Axiom engineers and mathematicians. The company did not name any specific models powering the swarms.
• The errors: Axiom reported 34 notable deviations from the published record. Most were minor: typos, table mistakes and dropped hypotheses. Two were substantive, both in load-bearing parts of the classification that had passed human refereeing.
• The Walter case: In the Unbalanced Group Theorem, the agents found explicit counterexamples to a closure assertion in John Walter’s 1986 proof, according to Axiom. The flagged case was PSL2(49), whose field involution centralizer is PGL2(7), while PSL2(7) sits outside Walter’s family.
• The quasithin case: Axiom said a lemma in the Aschbacher-Smith work on quasithin groups asserted an equality that was wrong, with SL2(5) as counterexample: one quantity was 1 where the asserted equality required 2. Replacing it with an inequality repaired the lemma, but a later argument needed a modified case split.
• New mathematics: Working around the gap, Axiom produced a new group-theory result, Preservation of simple tops, stated as Theorem 2.3 in its UGT paper, plus a formalized alternative argument. Axiom mathematicians later found a shorter deduction, Remark 9.5, that avoids Theorem 2.3 entirely.
• How checking worked: Lean verifies every dependency mechanically, while humans review the formal statements to confirm they express the intended classification. Engineers shared cached build results across workers and ran independent checks in parallel; finite computations were exported to separately checkable certificates, speeding verification by orders of magnitude.
• The limits: Axiom stated only the first-generation proof was formalized; the second-generation proof remains incomplete, with at least 12 volumes expected and 10 published through 2023. The company warned Lean can verify results resting on unproven hypotheses, and said the UGT development follows a different route from the original.
• Human review: Axiom said human mathematicians investigated the most significant reports in consultation with Richard Lyons and Ronald Solomon. The full proof, dependency map and errata list were published at cfsg.axiommath.ai, with the repository on GitHub; no repository license was stated.

Background:

The classification of finite simple groups sorts all finite simple groups into families plus 26 sporadic exceptions, the largest being the Monster. Assembled across decades of separate papers, it has long been cited as a proof no single mathematician has read end to end.

Between the lines:

The 34 deviations cut both ways. They show automated checking catching substantive gaps that survived human refereeing for decades, including in Walter’s 1986 argument. But Axiom’s own caveat matters: Lean will certify results standing on unproven hypotheses, and formalization counts as complete only when none remain. The second-generation proof, still unfinished in print, stays outside this result.

What’s next

Axiom said it will continue triaging and resolving the error reports with an advisory board including Richard Lyons, Dan Nakano and Ron Solomon, and will make the formalized results available for further mathematical work.