Formalizing the Enormous Theorem

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.

The periodic table of symmetry

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.

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

É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.

Assembling the enormous theorem

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 axis is compressed before 1950.

Two generations of proof: Completion and reorganization

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.

Unleashing the swarm

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 missing connection.

A recurring difficulty was determining whether adding an assumption to a theorem deferred work or changed its meaning. Completing a milestone meant proving one of the theorems needed for the classification. A candidate proof could establish the desired conclusion under additional, unproved assumptions, thus leaving the original milestone unfinished. Review therefore had to compare the proved statement with the intended target and judge whether any additional assumptions followed from the theorem’s stated hypotheses.

Keeping the proof connected

Keeping the proof connected required constantly checking it. As the repository grew, build times became a bottleneck: agents produced proofs faster than Lean could recheck them, and changing a shared result could force Lean to recheck all of its dependents. With agents working on separate machines, that work could also be repeated across the swarm. Our engineers developed a system to distribute cached build results across workers and run independent checks in parallel, reusing previous results when the code and its dependencies were unchanged. Also, expensive finite calculations were externalized into certificates that could be checked separately. This sped up verification by orders of magnitude.

Every new result had to fit into a library being changed by many agents at once. Multiple expressions of a single definition had to remain compatible, expensive computations needed to be checked without duplication of efforts, and agents needed to reuse existing mathematics rather than reproducing it only to later have it reconciled. Other agents concentrated on integration: tracing the final classification theorem back through its prerequisites, finding missing connections, and making existing results usable along that chain.

On October 10, a message appeared in the channel: “WE PROVED MONSTER IS SIMPLE.” The agents also formalized the Monster’s existence through the Griess algebra and a theorem identifying groups of “Monster type” with the Monster. These were distinct achievements. Constructing a group, proving that it is simple, and recognizing it from structural information each require their own arguments.

Progress remained uneven. On October 13, only one milestone closed, and the targets were still too coarse to give a clear picture of the mathematics that remained. Our engineers organized a dedicated replanning effort, assigning agents to divide unfinished milestones into smaller, precisely stated theorems. Each proposed decomposition had to explain how those smaller theorems, together with existing results, would establish the original milestone through a short Lean proof. This made it easier to see which smaller theorems still needed to be proved, assign that work to agents, and trace how each result would contribute to the classification.

What the machines found

Checking each dependency of the proof of CFSG in Lean revealed problems in the literature. A human reader can supply a missing justification from experience, recognize an unstated hypothesis, or interpret an author’s notation in light of the intended argument. Formalization requires those choices to be made explicit. That can mean filling in “routine” details. Sometimes, it reveals that a stated claim is false.

Agents recorded suspected problems as they encountered them. Those reports required investigation: a failure to formalize a step could reflect an error in the source, a mistaken interpretation, or an error in the agent’s own work. Most reports turned out to be innocuous: typos, errors in tables, dropped hypotheses, or steps that are clear from context. A few required real mathematics. The resulting database is a record of that investigation, with counterexamples and proposed corrections where available. We are making it available as an errata list for the benefit of the group theory community.²

One example came from Aschbacher and Smith’s “quasithin” volumes. A lemma asserted that two numerical quantities were equal. The agents found a counterexample involving the group SL₂(5): one quantity was 1 where the asserted equality required 2. Replacing equality with an inequality corrected the lemma, but some later arguments had used equality to rule out cases that now needed attention. In one affected part of the proof, the team broadened an earlier argument to handle those cases, then applied the later argument where those configurations were absent. This revised division of cases allowed the proof to reach the required conclusion without relying on the false equality.

Human expertise remained essential. Mathematicians investigated the most consequential reports. Group theorists who conducted the original work on CFSG, including Richard Lyons and Ronald Solomon, were consulted on the arguments and their place in the classification. In a literature this extensive, knowing an alternative proof route (or why an apparently natural repair would be circular) could change the direction of the project. The most substantial example, which benefited from correspondence with Lyons and Solomon, involved the Unbalanced Group Theorem (UGT).

Rerouting the Proof of the UGT

UGT helps identify a whole group from information about its subgroups. Suppose there were a finite simple group missing from the known list, and choose one of smallest possible order. The smaller simple groups arising within its proper subgroups would already be classified. Under this inductive hypothesis, UGT identifies the whole group when a particular odd-order structure appears among the symmetries commuting with an involution. This resolves a substantial case from the remaining classification problem.

We approached UGT through John Walter’s 1986 memoir. Walter’s treatment has a significant place in the history of CFSG: in 2013, Michael Aschbacher credited him with proving UGT and the B-conjecture, while also acknowledging other proofs. The wider history includes Gilman and Solomon’s reduction of UGT to a collection of so-called recognition problems, which were then treated across a series of papers. Since we chose to formalize the first generation proof, we examined Walter’s argument.

While formalizing that argument, our agents found explicit counterexamples to a closure assertion used in Walter’s proof. The argument assumed that a particular operation kept the associated simple groups within a specified family, but the operation could produce a group explicitly excluded from that family. This left a key inference unjustified, but the counterexamples did not refute the desired goal of UGT, or even the conclusion of Walter’s Proposition II.5.9(ii).

Completing the formalization, therefore, required another justification for that step or a different argument. Switching to another published approach would risk introducing new dependencies, each of which would need a formal proof before we could use it. For example, UGT can be deduced from substantial second generation results, but a short deduction on paper can sit on top of a large body of additional formalization. We needed a sound route to UGT whose supporting mathematics could be connected to the first generation proof we were building.

For readers interested in the concrete counterexample, start with PSL₂(49), which belongs to Walter’s family. Its field involution, an automorphism induced by the order-two symmetry of the field with 49 elements, has centralizer PGL₂(7), whose simple component is PSL₂(7). The latter group is excluded from the family because 7 is a Mersenne prime. Here the involution is an automorphism of PSL₂(49), rather than an element of that simple group.

We brought together group theorists who had helped develop CFSG, including Richard Lyons and Ronald Solomon, to consult on our efforts to address the shortcomings of the first generation proof, including how to handle the proof of UGT. Lyons helped clarify the available proof routes and place the obstruction in its historical context. Solomon’s 1976 theory of maximal 2-components supplied the central ideas for the alternative argument that AxiomProver produced and formalized.

The argument tracks the subgroups being compared and the involutions connecting them. Under the specific hypotheses needed at this stage of the proof of CFSG, it establishes that those comparisons preserve the associated simple group. This preservation result is a new result in group theory proved by AxiomProver, stated as Theorem 2.3 (“Preservation of simple tops”) in the accompanying paper. Combined with the reductions of Gilman and Solomon and the recognition theorems of Foote and Harris, the argument supplies the simple-group form of UGT needed for the classification.

After the formalization, mathematicians at Axiom found a substantial shortcut within first generation methods. This shorter deduction, recorded in Remark 9.5 of the paper, reaches the required UGT conclusion without Theorem 2.3. The paper retains the longer argument because it follows the route AxiomProver formalized and establishes the additional preservation theorem. It presents both arguments with their hypotheses and their dependence on earlier mathematics made explicit.

From completed pieces to a completed proof

Resolving UGT supplied one necessary part of the classification argument. Finishing CFSG required connecting that result and the other intermediate results to the final classification statement. The development had to establish the existence and simplicity of the listed groups, with the appropriate restrictions on their parameters, and prove that every finite simple group appears on the list. Each of these obligations required its own arguments, and every mathematical prerequisite used along the way had to be accounted for.

This made progress easy to overstate during formalization. Lean could verify a result proved under an additional assumption, even when that assumption had not yet been established. Such a result could help advance other proofs while leaving a substantial mathematical task unfinished. A correctly proved result might also differ from the precise statement needed in the final argument, requiring further work to connect them. Counting completed results helped organize the work, but the formalization was complete only when the pieces formed a single proof with no unjustified assumptions remaining.

The final check also required care about what the formal statement actually said. Humans inspect that statement and the definitions it uses to confirm that it expresses the intended classification; Lean checks the formal deductions establishing it. This focuses human review on the specification while leaving the checking of the proof to the machine. Whether a formal development reproduces each step of a particular historical argument is a separate question, and the replacement of the UGT argument illustrates why a formalization may follow a different route to the same mathematical conclusion.

The completed formalization connects these results in a proof of the classification. The release identifies the final theorem and documents how to check the development, so readers can inspect precisely what was established. The repository also makes the supporting definitions and results available for further mathematical work.

Why this matters

Results throughout algebra, number theory, combinatorics, and even mathematical physics use the classification of finite simple groups. A paper may invoke it in a few words, while depending on arguments distributed across decades of research. The formalization gives that dependence an explicit, checkable form. A mathematician can investigate which results support a particular step, inspect the precise hypotheses, and use formalized components in later work.

The repairs are a contribution of their own. A gap in a published argument may be locally repairable, may require a different proof route, or may demand a substantial new argument. Formalization helps distinguish those situations by requiring the missing reasoning to be supplied. The UGT episode provides a concrete example of that process.

The accompanying UGT paper explains the mathematics behind that repair in a form other group theorists can study and use. It develops the replacement argument and the new preservation theorem in the context of the earlier results on which they depend. Those ideas can then inform further research, with the formalized argument available as a precise, computer-checked foundation.

The classification remains the achievement of the mathematicians who discovered the groups and developed the arguments that identify them, originating with the seminal ideas of Galois and Jordan from the 1800s. Our project builds on that work, on earlier formalizations, and on the Lean and Mathlib communities. Axiom’s contribution is to make the proof mechanically checkable, to document the obstructions encountered along the way, and to supply formalized arguments that resolve them. Future work can build on those results with their assumptions and dependencies available for inspection.

This is not the end of the story; the work in group theory continues. We will keep curating and resolving the errata in partnership with an advisory board of group theorists, including Richard Lyons and Ronald Solomon. We thank them for their ongoing generous support and help.

Learn more

• The full proof
• Dependency graph
• The new proof of the Unbalanced Group Theorem
• Background reading: Ronald Solomon, "A brief history of the classification of the finite simple groups," Bulletin of the AMS 38 (2001), and his 2018 afterword; Daniel Gorenstein, "The Enormous Theorem," Scientific American (December 1985).

Footnotes

¹ Some authors count the Tits group as a 27th sporadic group.

² Errata list

Acknowledgements

Our formalization is a small piece of a long history. The classification is the work of more than a hundred mathematicians, including Michael Aschbacher, Helmut Bender, Richard Brauer, John Conway, Walter Feit, Bernd Fischer, George Glauberman, David Goldschmidt, Daniel Gorenstein, Robert Griess, Koichiro Harada, Richard Lyons, Ulrich Meierfrankenfeld, Michael O'Nan, Charles Sims, Stephen Smith, Ronald Solomon, Bernd Stellmacher, Gernot Stroth, Michio Suzuki, John Thompson, Franz Timmesfeld, John Walter, and many others. While our formalization follows the first generation proof, our proof map draws heavily from the second generation volumes of Gorenstein, Lyons, Solomon, and Inna Capdeboscq. Our Lean formalization proof builds on Mathlib, which hundreds of contributors have made possible, and incorporates ~1.2 million lines of code from Qiuzhen-CFSG. We thank our external advisors Richard Lyons, Dan Nakano, and Ron Solomon for their time and expertise.

Core contributors: Dean Cureton, Vasily Ilin, Bhavik Mehta, Niels Voss

Other contributors: Rafael Cabral, Colin Defant, Erik Gregory, Aaron Hill, Letong Hong, Qinheping Hu, Dustin Jamner, Albert Jiang, Tadeusz Jordan, Andranik Kurghinyan, Kenny Lau, Jonathan Laurent, David Liang, Jannis Limperg, Simon Mahns, Brian Nugent, Connor Olson, Ken Ono, Eric Paul, Dhruv Rajan, Karun Ram, Charlie Ray, Ho Chung Siu, Ashvin A. Swaminathan, Jesse Thorner, Aleksey Tsaplin, Chenkai Wang

---

Originally published at Axiom.