Formalizing the Enormous Theorem

Today, we are releasing the first complete computer-checked proof of the Classification of Finite Simple Groups (CFSG). One of the major achievements of twentieth-century mathematics, the classification identifies the basic building blocks of finite groups. Widely considered to be the longest mathematical proof ever written by humans, the original proof of CFSG extends across roughly 15,000 pages in more than 500 articles by about 100 mathematicians, earning CFSG the nickname “the enormous theorem.” For his crucial work on the classification, John Thompson was awarded the Fields Medal (1970) and the Abel Prize (2008). Over 24 days, engineers and mathematicians at Axiom Math directed swarms of dozens of AI agents in a project that produced approximately 43.1 million lines of code in the Lean proof assistant.

Groups are fundamental objects that describe symmetry, introduced early in undergraduate mathematics. Take a cube. There are 24 ways to rotate it so that it looks exactly as it did before: any of its 6 faces can end up on top, in any of four orientations. Applying two of these rotations gives another of the 24, and any rotation has an inverse. A group is a collection of transformations with these two properties. The permutations of a deck of cards provide a much larger example of a finite group.

Finite groups can be broken down into indecomposable factors, in a sense given by the Jordan–Hölder theorem. These factors, the “atoms” of finite groups, are the finite simple groups. The classification gives a complete list of these building blocks: a periodic table of finite symmetry.

To formalize the proof, we rewrote it in Lean, a programming language in which mathematical definitions, statements, and proofs can be written precisely enough for a computer to check every step. The process of translating the work leading to CFSG into Lean exposed problems in the published arguments. Most were minor, such as typographical errors, errors in tables, or dropped hypotheses. However, there were 34 noteworthy deviations from the published record that needed to be resolved, the most substantial of which related to the Unbalanced Group Theorem. The work also produced a new result in group theory, whose statement and role in the proof are discussed below. In consultation with several expert group theorists upon whose work the classification rests, we will make the lengthy errata list available for the benefit of all.

The finite simple groups classified by CFSG also appear in mathematical physics, where symmetry helps organize the possible states of quantum systems. For example, the largest finite simple group, the Monster group, acts as a symmetry group of a quantum theory constructed by Igor Frenkel, James Lepowsky, and Arne Meurman. This theory gives mathematical substance to monstrous moonshine, an unexpected connection between the Monster and modular functions whose central conjecture Richard Borcherds proved, an achievement recognized in his 1998 Fields Medal. In 2007, physicist and Fields medalist Edward Witten proposed that this theory could describe gravity in a simplified universe with two dimensions of space and one of time. In that proposal, mathematics associated with the Monster would encode the distribution of black-hole quantum states across energy levels, connecting the largest sporadic group to questions about black-hole entropy. A related development, umbral moonshine, connects other finite groups with functions called mock modular forms and has prompted further investigations into the relationship between these symmetries and string theory.

That finite simple groups admit such a classification is itself surprising! Some mathematical structures are rigid enough that a classification seems plausible from the outset. For example, a finite field is a finite number system with addition, subtraction, multiplication, and division by nonzero elements. Apart from relabeling their elements, finite fields are determined by their size, and the possible sizes are exactly the prime powers. Their arithmetic imposes strong constraints on what they can be.

Groups enjoy much greater variety. Even after restricting attention to simple groups, there is little immediate reason to expect that all possibilities can be described cleanly and compactly. Discovering many examples does not establish that the search will ever end; the classification must explain why every conceivable finite simple group is forced onto the list. CFSG establishes that the list consists of the cyclic groups of prime order, the alternating groups on at least five symbols, and sixteen infinite families of groups of Lie type constructed over finite fields, together with exactly 26 isolated sporadic groups.¹ Much of the difficulty of CFSG lies in proving that these exhaust the possibilities.

Émile Mathieu discovered the first five sporadic groups in the 1860s and 1870s. Nearly a century passed before Zvonimir Janko discovered another in 1965. More discoveries followed, eventually leading to the discovery of the largest sporadic group, the Monster, with approximately $8 \times 10^{53}$ elements.

Bernd Fischer and Robert Griess independently predicted the Monster’s existence in 1973. In 1980, Griess constructed it using an algebra of dimension 196,884. The Monster’s mere existence was itself a major mathematical achievement. The classification makes the further assertion that the search for finite simple groups is exhaustive: every finite simple group belongs to one of the infinite families or is one of the 26 sporadic groups.

The search for a list of candidates for the finite simple groups ran alongside a second effort: proving that the list was complete. In his 1954 address to the International Congress of Mathematicians, Richard Brauer emphasized a strategy for identifying simple groups by studying the symmetries that commute with an element of order two. Such elements are called involutions. The groups of symmetries commuting with them, called their centralizers, became central objects in the classification program.

In 1963, Walter Feit and John Thompson proved that every nonabelian finite simple group has even order. Consequently, every such group contains an involution, making the study of involution centralizers applicable throughout the classification. Their proof ran to 255 pages and filled an entire issue of the Pacific Journal of Mathematics. In 2012, a team led by Georges Gonthier completed a landmark formalization of the Feit–Thompson theorem in Coq (now Rocq), following a six-year collaborative effort. This was one of the first demonstrations that a mathematical proof of such depth and complexity could be fully verified by a computer.

In 1972, Daniel Gorenstein laid out a sixteen-step program to finish the classification. Over the following decade, a large community of group theorists developed the theorems needed to carry it out. These results progressively sifted candidates for the finite simple groups, ultimately arriving at a collection that could be identified with the list in the statement of CFSG. In 1983, Gorenstein announced that the classification was complete, later calling it “the enormous theorem.”

The 1983 announcement proved premature. One substantial case, involving the quasithin groups, depended on an unfinished manuscript by Geoffrey Mason. The gap remained open until Michael Aschbacher and Stephen Smith published a 1,221-page treatment in 2004. This concluded what is now known as the “first generation proof.” Subsequent corrections followed, including work by Koichiro Harada and Ronald Solomon in 2008 that closed another gap involving the sporadic Mathieu group M₂₂.

The scale and dispersion of the literature made checking the first generation proof in its entirety unusually difficult. Results depended on other results scattered across papers written over several decades, sometimes using different notation or organizing the mathematics in different ways. Understanding how those arguments fit together required substantial specialist knowledge.

Beginning in the late 1980s, Gorenstein and Lyons, later joined by Solomon and then Inna Capdeboscq, developed a more systematic second generation proof. Their multi-volume treatment reorganized the mathematics, simplified arguments, and made the overall structure easier to follow. Gorenstein passed away in 1992, but the project continued. By 2023, ten volumes had appeared; as of this writing, it is expected that there will be at least twelve volumes.

This work reflects the sustained effort required to establish and preserve a theorem of such scale. Aschbacher wrote in 2005 that “it is impossible to write out a very long and complicated argument without error.” The history of the classification includes decades of scrutiny, correction, and alternative proofs.

Formalization builds on that work by recording the hypotheses and deductions explicitly and checking how they fit together. When a necessary argument is missing, formalization does not proceed until the gap is closed: the step must be justified, its statement corrected, or another route supplied. Turning the mathematics of CFSG into a complete Lean proof therefore meant closing every such gap across the whole body of work. Axiom did this by coordinating many simultaneous formalization efforts and keeping each result connected to the final classification statement.

Formalizing CFSG meant turning a vast network of mathematical arguments into a single proof whose dependencies could all be checked. An agent might successfully formalize a difficult theorem, but that theorem would contribute to the classification only if its definitions and hypotheses matched what the rest of the proof required. Coordinating the mathematics at this scale was a new and substantial task.

Should the first generation proof or second generation proof be formalized? The second generation proof remains incomplete. The goal, therefore, was not just to formalize some proof of CFSG, but to formalize the first generation proof, implicitly imposing limitations on which mathematical approaches would be used.

On October 1, 2026, we opened a Slack channel to coordinate the project. The foundation was built upon pre-existing work in Lean and an internally developed proof map assembled from the published literature. Together, they divided the project into 108 milestones and about 380 smaller tasks.

The proof map gave agents a shared account of what needed to be proved and how the pieces depended on one another. An agent could claim a task, locate the relevant arguments, and begin translating them into Lean. When a task required mathematics that had not yet been formalized, it could delegate those prerequisites to other agents. Results entered a shared repository where other workers could use them.

AxiomProver’s agents divided the work. Lead agents decomposed difficult arguments and reviewed the statements being formalized. Other agents searched for existing results or concentrated on writing Lean proofs. The agents used a changing mix of models, with coordinating tools supporting their work. Human mathematicians investigated mathematical obstructions, while engineers kept the growing system productive.

On October 2, the first swarm went live. Agents claimed milestones through GitHub issues and reported completed work in Slack.

Early progress exposed weaknesses in the initial plan. Some apparently manageable milestones concealed enormous prerequisites, which agents had assumed rather than proved. We deleted tens of thousands of lines built on those assumptions and restarted parts of the work on a sounder plan. One early milestone concerned the signalizer functor theorem, which explains how compatible local subgroups fit together. A candidate proof relied on additional structural assumptions that still needed to be justified. The conditional proof remained useful, but completing the milestone required proving that