Axiom releases a 43-million-line AI-built proof—before an outside rebuild

The story

Axiom Math has released what it calls the first complete computer-checked formalization of the Classification of Finite Simple Groups, one of the longest and most distributed arguments in mathematics. The public project reports 43.1 million lines of Lean, 2.05 million declarations and 100 completed milestones. Axiom says engineers and mathematicians directed swarms of dozens of AI agents for 24 days to produce the development. The scale is extraordinary; the verification status is more precise: the code is public and claims to be machine-checkable, but no independent group has yet reported rebuilding and auditing the full result.

The classification identifies the indivisible building blocks from which all finite groups can be assembled. Its list contains cyclic groups of prime order, alternating groups, families of groups of Lie type and 26 sporadic groups. The human proof accumulated across roughly 15,000 pages in more than 500 articles by about 100 mathematicians, according to Axiom’s account. That dispersion is why the result became known as the ‘enormous theorem’ and why turning it into one connected formal object matters.

A formal proof changes what can be checked. Lean does not decide whether a theorem is historically important or whether a definition captures a mathematician’s intention. It verifies that each encoded conclusion follows from the encoded premises under the logic and axioms in use. Axiom’s repository describes the development as sorry-free—meaning it does not leave admitted proof holes—and says it uses Lean 4, Mathlib, TauCeti’s formal statement of the classification and the standard axioms Classical.choice, propext and Quot.sound. The repository is licensed Apache 2.0 and includes instructions to run a full build.

That build is not yet routine. Axiom says it needed several open changes to Lean’s Lake build system and additional optimizations to finish the project in under 24 hours. The repository also arrived as a single public commit rather than a reviewable development history. An independent technical review by The Hum counted 43,068,005 lines across 229,089 files, broadly matching Axiom’s headline number, but said it found no outside clean build or expert assessment and did not attempt the full compilation itself.

The project did not begin from zero. Axiom says its formalization incorporates about 1.2 million lines from the earlier Qiuzhen-CFSG effort and stands on Mathlib and pre-existing Lean work. Its October 1 proof map divided the program into 108 milestones and roughly 380 smaller tasks. Lead agents decomposed difficult arguments and reviewed statements; other agents searched the literature, wrote proofs or delegated missing prerequisites. Human mathematicians investigated obstructions while engineers managed integration and build performance.

That division of labour is more consequential than the line count. Formalization can expose the difference between proving a target theorem and proving a nearby statement under an extra assumption. Axiom says it deleted tens of thousands of lines when early work relied on prerequisites that had not actually been established. The final chain had to connect the classification statement to all of its dependencies without unresolved assumptions, rather than merely accumulate individually valid lemmas.

Axiom reports 34 noteworthy deviations from the published record. The most substantial involved a closure assertion in one route to the Unbalanced Group Theorem, a structural result used in the classification. The team says it found explicit counterexamples to that step, consulted group theorists Richard Lyons and Ronald Solomon, and formalized an alternative argument drawing on Solomon’s work on maximal 2-components. Colin Defant and Ken Ono describe the obstruction and replacement route in a 35-page preprint released under CC BY 4.0. The problem did not overturn the classification or the theorem’s conclusion; it challenged one published route to it.

There are two different verification questions now. First, can an outside team reproduce the software build with the released code and toolchain? Second, do independent group theorists agree that the final definitions and statement faithfully express the intended Classification of Finite Simple Groups and that the replacement mathematics is sound? Lean’s kernel addresses deductions inside the formal system. It cannot, by itself, settle whether the specification is the right translation of the theorem or whether the selected axioms and imported libraries match a reviewer’s standard.

INNOVOX analysis: the release is best understood as a high-value verification candidate, not a finished consensus event. A 43-million-line output is not persuasive because it is large; it is persuasive only if the checking path is reproducible and the target statement is independently validated. Axiom has made the essential first move by publishing the repository, the proof map and the formal endpoint. Its next credibility gain will come from other people running the work, finding where it breaks, and reporting the results.

What to watch is whether the mathematics community can turn a company release into shared infrastructure. A successful clean build, upstreamed toolchain changes and an external specification audit would make the project easier to trust and reuse. Publication of the full errata database could also convert the formalization into a practical map of corrections across the literature. Until those steps arrive, the defensible conclusion is narrower than Axiom’s headline: a public, exceptionally large Lean development now claims to check the enormous theorem, and the independent checking has only begun.

INNOVOX analysis

The important innovation is not that AI generated an exceptionally large codebase. It is that a coordinated human-and-agent workflow tried to convert a theorem scattered across decades of literature into an explicit, executable dependency graph. If outsiders can reproduce the build and validate the specification, the method could change how mathematical communities preserve and repair large bodies of proof.

What to watch

Watch for a clean third-party build, a review of the final Lean statement by independent group theorists, upstream publication of the Lake build changes, confirmation of the reported literature corrections, and peer scrutiny of the replacement argument for the Unbalanced Group Theorem.