The classification of finite simple groups, or CFSG, is widely regarded as one of the largest proof enterprises in modern mathematics. Built over decades by more than a hundred mathematicians, the argument is spread across hundreds of papers and books and runs to nearly 20,000 pages, putting full review beyond the reach of any single person or even a single team. That scale is the setting for FormaTheoria, an AI-assisted workflow aimed at formal verification on a much larger frontier.
Advocated by Shing-Tung Yau, the project was proposed by students from the leading class of Qiuzhen College at Tsinghua University together with research teams from the Yau Mathematical Sciences Center, the Institute for AI Industry Research, and the University of Warwick. Its goal is to let AI begin with raw mathematical literature, sort out dependencies, organize the underlying knowledge, construct formal proofs, and then pass the results to the Lean proof assistant for step-by-step checking.
According to the paper’s August 2026 snapshot, FormaTheoria had formalized four key theorems in Lean and produced more than 994,000 lines of interconnected code-based mathematics. The paper says a complete verification of CFSG is still a long way off, but presents the result as an important milestone on that path.
Why CFSG matters far beyond group theory
The name sounds abstract, but CFSG can be understood as a complete parts list for finite symmetry. A complicated finite symmetry structure can be broken down layer by layer into basic units that cannot be decomposed any further, and CFSG identifies what those basic units are.
Mathematicians often reduce hard problems to those basic units first and then handle them case by case using the classification. In that sense, CFSG works as infrastructure for many later proofs. If that infrastructure contains hidden gaps, a large body of downstream results could be affected.
The paper points to published surveys that make the breadth of those applications more concrete. In 2018, the American Mathematical Society published Stephen D. Smith’s book Applying the Classification of Finite Simple Groups: A User’s Guide. The book runs 231 pages across 10 chapters and maps out GFSG applications. The public table of contents for its final two chapters lists 14 numbered application topics, including distance-transitive graphs, the Frobenius conjecture, permutation group algorithms, subgroup growth in finitely generated groups, field extensions, coverings of Riemann surfaces, the Waring problem in group theory, expander graphs, and approximate groups.
The paper also notes high-level recognition from the broader mathematics community. At the 2014 International Congress of Mathematicians, Robert Guralnick, who later received the 2018 Cole Prize in Algebra from the American Mathematical Society, delivered an invited lecture titled Applications of the Classification of Finite Simple Groups.
Some of those applications sit inside major mathematical achievements. CFSG is a key part of the full proof chain for the restricted Burnside problem, whose solution earned Efim Zelmanov the 1994 Fields Medal. Smith’s book also lists the Waring problem on finite simple groups and expander graph directions as important CFSG applications, with representative papers published in Annals of Mathematics.
That repeated reuse is exactly why machine-checkable verification matters. The proof base behind CFSG comes from different decades, different authors, and different texts, often with incompatible notation, definitions, and implicit assumptions. A single citation can open another branch of literature. One major gap in the classification proof, the paper notes, was filled only more than 20 years later by a two-volume work totaling 1,220 pages. FormaTheoria therefore has to do more than check one step at a time; it must connect definitions, assumptions, and references across hundreds of documents into an unbroken proof chain.
How the workflow tackles large formal proof construction
Many AI math systems start with a cleanly posed problem where the definitions, tools, and statement are already prepared. FormaTheoria does not. It has to reconstruct the mathematical foundation behind the target from scattered literature before it can prove anything.
The paper identifies four main difficulties.
The full source set is unknown at the outset
A reference may lead to another paper, which then leads to more prerequisites. The project began with three main sources, then discovered 12 more during proof construction. Those later additions accounted for 65.6% of all pages consulted. FormaTheoria handles this by pausing the current proof whenever a missing prerequisite theorem appears, locating and formalizing that dependency, and then returning to the original task. Verified results are stored in a shared knowledge base so later proofs can reuse them.
Different texts do not fit together automatically
Authors use different definitions, symbols, and default conditions. Two definitions may be mathematically equivalent yet still fail to interoperate once written as Lean code. The system repeatedly compares the source text with existing code and builds the conversions needed to bridge them. It also protects statements that have already been verified and checks whether any repair changes later proofs. Only then can books and papers that were written independently begin to live inside one formal framework.
Passing Lean checks does not guarantee faithfulness to the source
Lean checks internal logic: whether a conclusion follows from premises and whether a proof is self-consistent. It does not decide whether the formal statement accurately reflects the original text. An AI system can omit a condition, confuse “for all” with “there exists,” or alter the claim itself. To handle that risk, FormaTheoria adds a separate review layer. One component drafts the Lean statement; another compares it back to the source line by line. Across 14 literature subsections analyzed in the paper, first-round translations were sent back for revision in 11 cases.
The literature can be wrong
Older texts may contain typographical errors, missing assumptions, or ambiguous phrasing. FormaTheoria preserves the original pages and traces backward once a contradiction appears later in the proof process. If the literature supports a correction, the system adds a condition or builds a compatibility relation. If the evidence is too weak, it records the issue and hands it to human mathematicians.
The workflow also has to manage very long-running tasks. A single interaction cannot carry the whole job, so the system keeps an evolving “proof map.” Hard goals are split into smaller auxiliary theorems, successful results are fed back up to the main theorem, and failed routes are recorded so the agent does not walk into the same dead end again.
Its parallelization strategy is also specialized. Independent tasks can run at the same time. If several tasks need the same prerequisite result, the system formalizes it once and lets the other tasks reuse it. Shared mathematical content that could affect a broad swath of later work is edited sequentially to limit conflicts. In the paper’s comparison experiments, this dependency-aware parallel mode delivered a 4.2x speedup on the tasks tested.
Put together, the workflow covers literature search, dependency recovery, source translation, proof construction, machine checking, independent review, conflict coordination, and escalation to human mathematicians when the system cannot decide. The paper frames that chain as a direct response to the real obstacles inside very large proof projects.
Four key theorems, seven months, and a large dependency graph
FormaTheoria submitted its first code on Jan. 22, 2026. By Aug. 2, 2026, it had connected a key theory path reaching the Bender–Suzuki theorem. Along that route, it formalized the Feit–Thompson odd order theorem, the Glauberman Z* theorem, the Brauer–Suzuki theorem, and the Bender–Suzuki theorem.
Those theorems are not isolated checkpoints. They form an important connected route inside the classification of finite simple groups, and later proofs rely heavily on the mathematical base laid down by earlier ones.
The project snapshot reported in the paper includes:
- more than 994,000 lines of Lean code,
- more than 850 code files,
- 15 books and papers consulted across 1,037 pages, with about two-thirds discovered during the proof process itself.
The line count only shows one side of the project’s scale. Tracing backward from the Bender–Suzuki theorem, the system had built a proof network with 30,298 mathematical statements and 186,187 dependency links, with the longest dependency chain reaching 458 layers. If related material from Lean’s base library is included, the network grows to 74,922 statements and more than 1.44 million dependencies.
The paper says the project’s run profile is also long-horizon in a literal sense. The longest single agent execution it records lasted 9.17 days. During that run, the system compressed and reorganized accumulated information 606 times while retaining the current proof target, completed results, and unresolved items.
The paper contrasts this with earlier large-scale formalization work done mainly by humans. As a historical reference, it points to a previous Rocq formalization of the Feit–Thompson theorem that took about 15 people six years to complete. FormaTheoria, by comparison, finished the full content of that human project in seven months and then extended the formalization effort to other key theorems. Seven months is still long for an AI-agent run, but much shorter than the timeline described for the earlier human-led effort.
Formalization also exposes problems in the source literature
Mathematics papers are usually written for readers already familiar with the area. Authors often omit conditions introduced earlier or assume readers can recognize equivalence between different definitions. Small typographical or symbolic mistakes may also be ignored or mentally repaired by human readers. FormaTheoria works differently. When it translates literature into Lean, every definition, assumption, and inference step has to be explicit. That line-by-line pressure makes hidden problems stand out.
The paper records several kinds of issues: inconsistent definitions for the same concept across sources, theorem statements missing necessary assumptions, divisibility conditions written in the wrong place, and index errors inside proofs. Some can be corrected from context. Others are left for mathematicians to judge.
A mismatch in “type I maximal subgroup” definitions
One example comes from two sources on the odd order theorem. Both define “type I maximal subgroup,” but one source requires a certain property to hold for every complement structure, while the other only requires the existence of one complement structure with that property. Formally, the first is stronger than the second, so the two definitions cannot be merged directly. FormaTheoria detected the difference during formalization and then used the Schur–Zassenhaus theorem to show that the two definitions are equivalent in this setting, creating a bridge between the texts.
A missing assumption in a lemma of Peterfalvi
Another case involves a lemma by Peterfalvi. Its formal statement omits the assumption that the order of a certain group is odd, even though the later proof depends on it. The broader argument still works because that condition had already been ensured earlier when the lemma was applied, but Lean does not fill in that background automatically. By tracing the proof path and use sites, FormaTheoria added the missing condition explicitly to the theorem statement.
More direct errors in print
The project also found more straightforward mistakes. One definition wrote M where H should have appeared, and two reference sources carried the same error. A theorem in Huppert placed a factor d into the wrong divisibility condition; the system found a counterexample, halted the proof, and referred the issue to mathematicians, who then confirmed the correct condition. In a proof by Higman, a list of basis vectors was indexed from u₀ to uₘ even though the correct range should end at uₘ₋₁. The system identified and corrected that subscript error while proving the result.
For the paper, these examples show another value of machine-checked work in large mathematics projects. FormaTheoria is not only turning proofs into code. It is also conducting a fine-grained audit of the literature, recording where a problem appears, what later arguments require, which sources justify a correction, and whether that change affects any other result.
Project status and the model of collaboration it proposes
FormaTheoria has not completed a full formalization of the classification of finite simple groups. The paper is explicit that the final goal remains distant. Still, it says the project is accelerating toward that target.
The current results, as described in the paper, suggest that AI can maintain and expand a large mathematical environment over months, track complex dependencies across multiple texts, and build an interconnected theory system under strict verification. In that account, the role of AI begins to move from solving isolated math problems toward participating in the construction of organized mathematical knowledge.
The work also aims to leave behind reusable infrastructure. Traditional literature can tell readers where a proof is written. Formalized code can additionally record what each conclusion depends on, how different sources connect, and which issues were corrected, while organizing verified definitions, lemmas, and proofs into reusable modules.
The paper adds that explanation, search, and visualization tools could later make that knowledge network easier to navigate, helping researchers understand the structure of CFSG more quickly, reuse existing results, and possibly support mathematicians exploring new links and new theorems.
The FormaTheoria team presents the project as a possible human-machine collaboration model for the AI era: humans choose worthwhile problems and make key judgments, AI handles large-scale search and derivation, and formal systems ensure that every accepted step can be checked again. For proofs so large that no individual can realistically re-verify them from scratch, the paper argues that this combination may offer a new way to manage mathematical knowledge at extreme scale.
The project status and quantitative results cited in the article come from the paper’s August 2026 completion snapshot.