Axiom says AI agent swarms machine-checked math's longest proof — the classification of finite simple groups — in 24 days

The AI startup Axiom says it has produced the first complete computer-checked proof of the Classification of Finite Simple Groups (CFSG) — the result that lists every “atom” of finite symmetry and whose original human proof spans roughly 15,000 pages in more than 500 articles by about 100 mathematicians.

How it was done

According to Axiom’s 26 October write-up, engineers and mathematicians directed swarms of dozens of AI agents for 24 days (from 1–2 October 2026), producing about 43.1 million lines of code in the Lean proof assistant, which checks every logical step. The work followed the “first-generation” proof, built on Mathlib, and was split into 108 milestones and about 380 tasks. Along the way agents proved, among other things, that the Monster group is simple.

What the machines found

Most problems uncovered in the literature were minor (typos, table errors, dropped hypotheses), but Axiom reports 34 noteworthy deviations from the published record. The biggest concerned the Unbalanced Group Theorem: agents found counterexamples to a step in John Walter’s 1986 argument, and the team built an alternative route, including a new result its prover established, after consulting group theorists Richard Lyons and Ronald Solomon. Axiom says it will publish an errata list.

Caveats

Lean checks the deductions, but humans still have to confirm that the formal statements and definitions really capture the intended theorem. Media reports as of 27 October noted that no outside group had yet independently rebuilt the full proof; Axiom has published the repository and build artifacts to make that possible. The claims here come from the company’s own report.