AI agents helped Axiom turn the longest proof in math, about 15,000 pages, into code a computer checked line by line, in 24 days.

Axiom, an AI math startup, says it has produced the first complete computer-checked proof of the Classification of Finite Simple Groups (Axiom on X, Axiom).

The theorem lists every basic "building block" of symmetry in math, and its original proof runs to roughly 15,000 pages across more than 500 articles by about 100 mathematicians, which is why it's nicknamed "the enormous theorem." Over 24 days, Axiom's engineers and mathematicians directed swarms of dozens of AI agents that wrote about 43.1 million lines of code in Lean, a programming language where a computer checks every step of a proof. Translating the proof this way turned up problems in the published record: most were typos or dropped assumptions, but Axiom counts 34 "noteworthy deviations," the biggest involving a piece called the Unbalanced Group Theorem, and says the work also produced a new result in group theory.

The code is public under an Apache 2.0 license, and the project says it uses only Lean's standard axioms and has no unfinished steps (GitHub, project site).

What to watch: the computer checks the logic, but people still have to confirm the formal statement means what mathematicians mean by the theorem. Axiom says it will publish its full list of errors after consulting group theorists, and outside experts haven't weighed in publicly yet. It comes a day after OpenAI's Lean-checked math claims, so expect "AI checked it" to become a standard bar for AI math results.