43.1 Million Lines of Lean Code in 24 Days: AI Formally Verifies the Classification of Finite Simple Groups

Forum topic · QianXun · 2026-11-01

Summary

A multi-agent system developed by Axiom completed a full formal verification of the Classification of Finite Simple Groups (CFSG) in 24 days, producing 43.1 million lines of Lean code — roughly an 86-meter stack if printed on A4 paper. CFSG, known as the 'Enormous Theorem,' spans about 15,000 pages of proofs written by roughly 100 mathematicians across 500+ papers over half a century. The project, launched October 1, broke the proof into 108 milestones and ~380 subtasks, reusing ~1.2 million lines from Mathlib and Tsinghua's Qiuzhen CFSG project, and finished on October 26 with the Lean kernel confirming the full chain from base axioms. Notably, verification became a bottleneck (solved with a custom distributed cache), and the AI found 34 notable discrepancies in the human proofs, including a counterexample (PSL2(49)) to a key closure claim in a theorem on unbalanced groups, prompting a new formalized proof route with input from Richard Lyons and Ronald Solomon. The project is not yet independently verified, and Axiom has not disclosed the models or compute used.

Overview

Axiom's multi-agent system formally verified the Classification of Finite Simple Groups (CFSG) — the so-called "Enormous Theorem" — in 24 days, producing 43.1 million lines of Lean code. Printed single-sided on A4 paper at 50 lines per page, the codebase would stack about 86 meters high (an earlier 1,300-meter estimate in the original post was a calculation error: 43.1 million lines ≈ 862,000 pages ≈ 86 meters at ~0.1 mm per page).

The Theorem's Weight

CFSG's proof spans roughly 15,000 pages across 500+ papers by about 100 mathematicians over half a century.
Completion was announced in 1983, but the quasithin group case rested on an unfinished manuscript until Aschbacher and Smith published a 1,221-page fix in 2004.
No one has ever read the complete proof; it has been sustained by division of trust across the mathematical community. Core team member Vasily Ilin noted that most people who truly understand the proof are retired or deceased.

Timeline

Oct 1: Project launch; humans decompose the proof into 108 milestones and ~380 subtasks.
Oct 2: The agent swarm goes live — a lead agent decomposes hard arguments; other agents retrieve existing results or write Lean code, with unproven prerequisites automatically outsourced.
Oct 10: "We proved the Monster group is simple" in the team channel.
Oct 26: Completion; the Lean kernel confirms the entire chain from foundational axioms to the classification theorem.

Engineering details: ~1.2 million lines reused from Mathlib and Tsinghua's Qiuzhen College CFSG project; Lean v4.35.0-rc3; full build under 24 hours. By declaration count, this is the largest open-source software project ever — exceeding the Linux kernel and Chromium.

Two Underrated Details

1. Verification became the bottleneck. AI generated proofs faster than Lean's dependency rechecking could handle, forcing the team to build a custom distributed cache that sped verification by orders of magnitude. For the first time in formalization history, checking lagged generation as an engineering problem. 2. 34 notable discrepancies found in the human proofs. Most were typos, table errors, or missing hypotheses. The hardest: in the theorem on unbalanced groups, following John Walter's 1986 argument, an agent found an explicit counterexample PSL2(49), invalidating the original key closure assertion. The team consulted Richard Lyons and Ronald Solomon (participants in the original classification); based on Solomon's 1976 theory, AxiomProver constructed and formalized a new route, proving a previously unknown group-theory result (preservation of "simple tops," preprint on Hexagon). Mathematicians later found a shorter classical route; both appear in the paper. The machine acted, for the first time, as a collaborating researcher rather than a verifier.

Context Among Recent Milestones

August: Axiom formalized the 246 prime gap theorem (verifying a human proof).
Late October: Resolution's agents auto-formalized Hironaka's resolution of singularities in about a week — 600,000 lines, $135k in token costs (self-reported).
Oct 26–27: OpenAI and Anthropic published deterministic algorithm results overturning ETH with Lean machine verification.

The bottleneck has moved from "whether it's possible" to "how long and how much." Caveats: the proof has not been independently reconstructed; Axiom has not disclosed which models or how much compute were used; whether the formalized statements faithfully express CFSG as mathematicians conceive it still awaits review by group theorists — an invitation the company itself issued.

What Mathematicians Are Digesting

Ken Ono posted a tribute to his father (who passed away this January), recalling how his father introduced him to the giants of group theory, and wept at the human-machine crossing of the finish line. Some researchers are devastated that their work was scooped by AI; others mourn the loss of "the joy of discovery." Behind the emotion is a structural shift: when verification can be done at scale, mathematicians move toward choosing which problems deserve formalization and feeding results back into human understanding. Yu Deng drew the sharpest boundary on a podcast: problems with proofs, and problems whose proofs humans can understand — these used to coincide; now they diverge.

> Tip: Finite simple groups are the "building block" symmetry structures from which all finite groups are assembled. The classification theorem is a complete census — a periodic table of sorts. The Monster group is the largest sporadic simple group, with about 8 followed by 53 digits of elements.

References

36Kr: "AI Completes the Largest Mathematical Proof in Human History" (Oct 31)
DeepTech: "24 Days to Write 43.1 Million Lines of Code" (Oct 29)
Axiom official research page and GitHub repo AxiomMath/CFSG
i10X News: commentary on the 34 discrepancies, the 2.05 million declarations, and the absence of independent replication
Import AI 478: Resolution's singularity resolution formalization (600k lines / $135k)

In one line: 15,000 pages took half a century; 43.1 million lines took 24 days. The paper tower's true height is 86 meters — and the mathematics beneath both towers is the same.