15,000-Page Mathematical Proof Verified by an AI Swarm in 24 Days, Catching More Than 2,000 Errors Along the Way

On October 27, Axiom announced the completion of a Lean formal verification of the Classification of Finite Simple Groups (CFSG). This is the longest proof in the history of mathematics: about 15,000 pages, written by more than 100 mathematicians over 30 years, and previously no single person had read it all the way through.

A group of AI agents completed the verification in 24 days. They divided up the work themselves, claimed tasks, reviewed one another, and collaborated on GitHub like an engineering team. In the end, every step was checked by the Lean kernel—the conclusion does not rely on trusting the AI; it was proven correct by machine.

The project produced 43.1 million lines of Lean code, making it the largest Lean codebase to date. In the process, the AI found more than 2,000 errors missed by humans, 34 of which constituted substantive deviations.

CFSG attempts to list all finite simple groups—the indivisible “atoms” of finite groups, analogous to a periodic table of symmetry. The theorem claims that every finite simple group is either part of one of the infinite families—cyclic groups of prime order, alternating groups, and groups of Lie type—or is one of the 26 sporadic groups, including the largest sporadic group, the “Monster,” which has about 8×10^53 elements. The proof of this theorem is scattered across more than 500 papers, with extremely complex dependencies, so doubts about its correctness have long persisted.

Source: S. D. Smith; ATLAS of Finite Group Representations.

The timeline shows the journey from Galois to Axiom:

Lean is a proof-assistant language in which mathematical definitions, statements, and proofs can be made precise enough for a computer to check every step. Formalization means translating the entire proof into Lean code, forcing every logical gap to be filled.

Axiom provided the agents with a manually constructed proof map, breaking the entire proof into 108 milestones and about 380 tasks. The agents claimed tasks, found relevant arguments, translated them into Lean, and could delegate to other agents to prepare prerequisites. Many problems arose along the way: some early milestones concealed enormous assumptions, and the team deleted more than 10,000 lines of code built on mistaken assumptions and started over. Engineers also developed distributed caching and parallel checking to keep build time from becoming a bottleneck.

On October 10, a message appeared in the channel: “We proved that the Monster is simple.” The agents also formalized the existence of the Monster via the Griess algebra and proved a theorem identifying “Monster-type” groups as isomorphic to the Monster.

Milestone completion progress:

The most interesting discovery came in the Unbalanced Group Theorem (UGT). This theorem helps identify an entire group from information about its subgroups. Axiom tried to formalize John Walter’s 1986 proof, and the agents found an explicit counterexample: a closure assertion assumed that a certain operation would keep the relevant simple groups within a family, but the operation could produce groups excluded from that family. For example, starting from PSL₂(49), the centralizer of a field involution contains PSL₂(7), and 7 is a Mersenne prime, which is excluded from the family.

In other words, Walter’s argument had a real gap. But the counterexample did not overturn UGT itself. In consultation with Richard Lyons and Ronald Solomon (major contributors to CFSG), Axiom had the agents prove a new result (Theorem 2.3, “Preservation of the Simple Top”) based on Solomon’s 1976 theory of maximal 2-components, replacing the original step. This new result also formed the core of the UGT paper.

Aschbacher wrote in 2005: “It is impossible to write a very long and complicated argument without making mistakes.” This formalization turned that statement into a concrete case.

What does this mean for software engineering? Today’s coding agents can write large amounts of code, but every line still requires human review. If a swarm of agents can coordinate to handle a 40-million-line mathematical proof and prove every step correct, the same approach can be applied to software. Entire codebases could be written, checked, and delivered by agents without humans hunting for bugs—this is precisely the direction Axiom is heading next.

One commenter wrote: “The self-checking part is crazy. Imagine applying this level of verification to production code.” Another said: “What’s interesting isn’t just catching 2,000 errors, but that checking is separate from writing. Code is the same: the agent that writes a PR shouldn’t be the one that approves it.”

The complete proof map and code have been made public on GitHub, and Axiom invites group theorists and the Lean community to rerun the verification. This is the first time in the history of mathematics that the work of more than 100 mathematicians has been completely machine-checked. Whatever your attitude toward AI formalizing mathematics, one fact can no longer be ignored: a proof no human had read was read by AI—and read very carefully.