Axiom formalizes the “enormous theorem” with a 43.1-million-line Lean proof

What is changing?

Axiom Math said in an October 26 announcement that it released the first complete computer-checked proof of the Classification of Finite Simple Groups. According to the company, engineers and mathematicians directed dozens of AI agents that produced about 43.1 million lines of Lean code over 24 days. The “first” and “complete” descriptions are Axiom’s claims; the published proof and dependency graph are available for inspection rather than treated here as independent academic validation.

The project translates a classification spread across roughly 15,000 pages and more than 500 papers into formal dependencies. Axiom says it found 34 noteworthy deviations from the published record, with the largest issue surrounding the Unbalanced Group Theorem, and developed a new group-theory result while resolving that part.

The significance is not only the proof’s size, but the way agents divided work through a shared proof map. Human experts investigated disputed steps while Lean checked each deduction, showing why traceable dependencies and verifiable deliverables matter more than raw output counts in scientific-agent systems.