The Classification of Finite Simple Groups (CFSG) is arguably one of the largest proof projects in modern mathematics.
This proof, completed over decades by over a hundred mathematicians, is scattered across hundreds of papers and monographs, with a total volume approaching 20,000 pages, far exceeding the capacity for any single individual or team to fully review.
Against this backdrop, introducing AI-assisted large-scale formal verification has become an essential new path to explore.
To advance AI for Math, under the advocacy of Shing-Tung Yau, a research team composed of students from the Qiuzhen Class (Leading Class) at Tsinghua University, and researchers from the Yau Mathematical Sciences Center, the Institute for AI Industry Research (AIR) at Tsinghua University, and the University of Warwick, has proposed FormaTheoria—an AI-assisted workflow for mathematical research: enabling AI to start from raw mathematical literature, automatically organize dependencies, integrate knowledge systems, construct formal proofs, and finally hand them over to the Lean proof assistant for step-by-step verification.
As of August 2026, FormaTheoria has completed the Lean formalization of four key theorems, generating over 994,000 lines of interrelated code-based mathematical theory. While there remains a long journey to fully verifying the CFSG, this achievement marks a significant milestone towards that ultimate goal.
CFSG Provides the Foundational Framework for Numerous Important Mathematical Results
The "Classification of Finite Simple Groups" sounds quite abstract. Simply put, it's like a "basic parts list" for finite symmetries: any complex finite symmetric structure can be decomposed layer by layer into fundamental units that cannot be further split; the role of CFSG is to tell mathematicians exactly what these basic units are.
Typically, mathematical research first breaks down a complex problem to these fundamental units, then handles them category by category according to the complete list provided by CFSG. Therefore, CFSG becomes an infrastructure that other proofs can readily invoke. If this "infrastructure" harbors hidden flaws, a vast number of subsequent results built upon its conclusions could be affected.
Some professional surveys provide quantitative evidence for the applications of CFSG. The American Mathematical Society published Stephen D. Smith's monograph "Applying the Classification of Finite Simple Groups: A User's Guide" in 2018, spanning 231 pages across 10 chapters, detailing application scenarios of CFSG. The last two chapters' public table of contents lists 14 numbered application topics, including distance-transitive graphs, the Frobenius conjecture, permutation group algorithms, subgroup growth of finitely generated groups, field extensions, covers of Riemann surfaces, the Waring problem in group theory, expander graphs and approximate groups, among others.
The application value of CFSG has also received recognition at the highest levels of the international mathematical community. The 2014 International Congress of Mathematicians invited Robert Guralnick, winner of the 2018 AMS Cole Prize in Algebra, to give a plenary lecture titled "Applications of the Classification of Finite Simple Groups."
These applications include highly influential and significant results. CFSG is a key link in the complete proof chain for the restricted Burnside problem; Efim Zelmanov received the 1994 Fields Medal for solving this problem. Smith's monograph also lists the Waring problem for finite simple groups and expander graphs as important application areas of CFSG, with representative papers published in journals like Annals of Mathematics (Waring problem; diameters of finite simple groups and their applications). These examples show that CFSG already supports a series of important works that have garnered top academic awards and appeared in premier mathematical journals.
In this sense, CFSG has become a foundational system that is repeatedly used. As downstream results accumulate, verifying its correctness and verifiability becomes increasingly critical. Performing machine-verified, traceable, and repeatable checks on CFSG carries significance beyond group theory itself.
However, the difficulty lies in the fact that this foundational proof comes from different eras, authors, and literature, often using inconsistent notation, definitions, and default conditions. A single citation might even point to another entire body of literature. Historically, a major gap in the classification proof wasn't filled until over twenty years later by a two-volume monograph totaling 1,220 pages. FormaTheoria not only needs to verify step-by-step reasoning but also check whether definitions, conditions, and references across hundreds of documents can be seamlessly connected, ultimately forming an unbroken chain of proof.
How AI Advances Ultra-Large-Scale Proof Projects
Many AI math systems are presented with a prepared problem, where the question, definitions, and tools are all set, and the AI only needs to find the proof. But FormaTheoria is different; it first needs to reconstruct the mathematical foundations behind the problem from scattered literature before completing the proof. This work primarily faces four challenges:
First, the system doesn't know in advance how much material needs to be consulted.
A single citation might lead to another paper, which in turn cites more prerequisite work. The project initially had only 3 main sources, but during the proof process, an additional 12 sources were discovered; this supplementary material accounted for 65.6% of all pages consulted. FormaTheoria's approach is: whenever a missing prerequisite theorem is found, it pauses the current proof, looks up and formalizes that dependency, then resumes the original task. Results already verified are stored in a unified knowledge base for reuse in subsequent proofs.
Second, different documents are difficult to directly piece together.
Different authors use different definitions, symbols, and default conditions. Two definitions might be mathematically equivalent, but when written into Lean code, they might be incompatible. FormaTheoria repeatedly compares original texts and existing code to build necessary conversion relationships. Simultaneously, the system protects already verified mathematical statements and checks whether each fix might affect subsequent proofs. This way, multiple independent books and papers can gradually integrate into the same theoretical framework.
Third, code passing checks may still misinterpret the original text.
Lean only checks whether the proof logic is self-consistent and whether conclusions follow from premises; it cannot judge whether a conclusion faithfully represents the original text. The AI might miss a condition, confuse "for all" and "there exists," or even incorrectly modify the conclusion. For this, FormaTheoria has a dedicated, independent review checkpoint: the translation component first writes the Lean statement, then the review component cross-checks it item by item against the original text. In the 14 literature sections analyzed in the paper, the first-round translations for 11 sections were sent back for revision. This independent review mechanism thus serves as a second "safety net" beyond machine verification.
Fourth, the original literature itself may have issues.
Old literature might contain typographical errors, missing conditions, or ambiguous phrasing. FormaTheoria preserves the original pages and backtracks to investigate when contradictions arise in later proofs. If the literature supports a correction, the system adds the condition or establishes compatibility. When evidence is insufficient, the system records the issue for judgment by mathematical professionals.
Beyond this, the project also requires the AI to maintain pace over long cycles. A single conversation cannot hold the entire task. Therefore, FormaTheoria uses a continuously updated "proof map" to manage progress: challenging goals are broken down into smaller auxiliary theorems; successful results aggregate back to the main theorem layer by layer; failed routes are also recorded to prevent the system from repeatedly entering the same dead end.
The project also features special designs in its parallelization strategy. Independent tasks can proceed simultaneously. When multiple tasks encounter the same prerequisite result, the system completes it only once and allows other tasks to reuse it. Public mathematical content that might have widespread impact is modified sequentially to avoid conflicts. The paper's controlled experiments show that this dependency-aware parallel approach achieved a 4.2x speedup on the tested tasks.
Thus, FormaTheoria forms a complete workflow chain: finding literature, completing dependencies, translating original text, constructing proofs, machine verification, independent review, coordinating conflicts, and handing uncertain issues to mathematical professionals. Each step has clear responsibilities and is documented. This design specifically addresses the practical difficulties that arise in ultra-large-scale proof projects, empowering AI to gradually connect scattered mathematical literature into a checkable, traceable, and sustainably expandable theoretical system.
△
Seven Months, Four Key Theorems, Nearly a Million Lines of Verifiable Code
On January 22, 2026, FormaTheoria first submitted code. By August 2, 2026, the project had established a key theoretical chain extending to the Bender–Suzuki theorem, having sequentially completed proofs for the Feit–Thompson odd-order theorem, Glauberman Z* theorem, and Brauer–Suzuki theorem.
These four theorems are not isolated; they form an interconnected, important pathway within the CFSG, where the proof of a later theorem often builds upon the vast mathematical foundation laid by the former.
The project snapshot upon completing these proofs includes:
- Over 994,000 lines of Lean code ;
- Over 850 code files ;
- The system consulted 15 books and papers, totaling 1037 pages , about two-thirds of which were gradually discovered during the proof advancement.
Of course, lines of code only show one aspect of the project's scale. Tracing backwards from the Bender–Suzuki theorem as the endpoint, the project has formed a proof network containing 30,298 mathematical declarations and 186,187 dependency relations, with the longest dependency chain reaching 458 layers. Including relevant content from the Lean base library, this network expands to 74,922 declarations and over 1.44 million dependency relations. It can be said that behind the nearly million lines of code lies an intricately intertwined, tightly linked proof network. This research indicates that AI agents, with the combined force of machine verification and layered review, can already continuously advance large, ultra-long-range mathematical projects.
The project's actual runtime also features an ultra-long-range characteristic. The longest single agent execution recorded in the paper lasted 9.17 days, during which the system performed 606 compactions and reorganizations of accumulated information while consistently retaining the current proof goals, completed results, and unresolved issues. These data show that the project manages an evolving, ultra-long-range proof network; a single generation or one conversation cannot cover such a complex process.
Previously, large-scale mathematical formalization relied heavily on manual effort, typically requiring multiple researchers to collaborate for years. A historical reference for comparison: the previous Coq formalization of the Feit–Thompson theorem took about 15 people six years to complete. In contrast, FormaTheoria completed the entire content of that manual project within seven months and further extended formalization work to other key theorems. Seven months remains an extremely long runtime for a single AI agent task, but compared to traditional manual formalization, AI intervention significantly shortens the project's timescale.
△
Formalization Brings Hidden Issues in Literature to Light
Mathematical literature is typically written for researchers familiar with the field. Therefore, authors often omit conditions mentioned earlier or assume readers can recognize equivalence between different definitions. Minor typographical or symbolic errors are also often naturally ignored or corrected during human reading. But FormaTheoria is different; when translating literature line by line into Lean code, every definition, every condition, and every step of reasoning must be written clearly and unambiguously. It is precisely this rigorous requirement for line-by-line verification that makes problems originally hidden in the source literature become apparent.
The paper details various literature issues discovered by the project, including inconsistent definitions for the same concept across different sources, omitted necessary conditions in theorem statements, misplaced divisibility conditions, and even errors in subscripts within proofs. Some issues could be automatically corrected based on the context of the literature; insufficient evidence would be passed to mathematicians for further judgment.
A typical case comes from two sources on the odd-order theorem. Both define "type I maximal subgroup," but the difference is: one requires a certain property to hold for "every complement structure"; the other only requires "there exists a complement structure" satisfying that property. Formally, the former is clearly stronger than the latter, so the two definitions cannot directly connect. FormaTheoria acutely identified this discrepancy during formalization, then used the Schur–Zassenhaus theorem to prove the two definitions are actually equivalent in this context, successfully building a bridge between the two sources.
Another case involves a lemma from Peterfalvi. The formal statement of this lemma omitted the premise condition "the order of a certain group is odd," yet subsequent proofs actually rely on this condition. Although this condition was already guaranteed by preceding context when applying the lemma later, and the overall argument wasn't broken, Lean won't automatically fill in this background information. After tracing the lemma's proof path and usage locations, FormaTheoria automatically added the missing condition to the theorem statement, making the entire formalization chain more complete and reliable.
△
The project also found more direct literature errors. One definition incorrectly wrote an object as M instead of H, and two reference sources retained the same mistake. A theorem by Huppert placed a factor d in the wrong divisibility condition; the system found a counterexample, halted the proof, and passed the issue to mathematicians for verification, who confirmed the correct condition. A proof segment by Higman incorrectly wrote the indexing of a basis set of vectors as from u0 to um, where the correct range should be to um−1; this subscript error was automatically identified and corrected by the system during proof construction.
These cases reflect another important layer of value that machine verification brings to large mathematical projects. FormaTheoria, while constructing formal proofs, also performs fine-grained scrutiny of original literature: it records where issues appear, what conditions subsequent proofs require, which literature provides the basis for corrections, and whether modifications affect other results. For CFSG, constituted by hundreds of interlinked documents, this traceable review mechanism can transform details previously filled in by reader experience into mathematical evidence that can be explicitly checked.
Future Outlook
FormaTheoria has not yet completed the overall formalization of the CFSG; there remains a long journey towards the final goal. The project is accelerating, steadily progressing toward fully formalizing one of modern mathematics' most massive proof projects. Current results show that AI can already maintain and expand large-scale mathematical environments over months, track complex dependencies across multiple documents, and construct interconnected, objectively substantial theoretical systems under strict verification. The boundaries of AI capability are thus beginning to extend from solving isolated mathematical problems to participating in the systematic construction of mathematical knowledge.
This work will also form a sustainably expandable, reusable mathematical infrastructure. Traditional literature can only tell readers "where the proof is written"; formalized code further records "what each conclusion depends on," "how different sources connect," "which issues have been corrected," and organizes verified definitions, lemmas, and proofs into knowledge modules directly usable for subsequent research. Once augmented with explanatory, search, and visualization tools in the future, this knowledge network could help researchers understand the overall structure of CFSG faster, reuse existing results, and even provide strong support for human mathematicians exploring new connections and discovering new theorems.
The FormaTheoria project team aims to explore a human-machine collaboration model for the AI era: humans are responsible for identifying worthwhile research problems and making key judgments, AI undertakes large-scale search and deduction, and formal systems ensure every accepted step can be re-examined. When a proof grows too large for any individual to review from scratch, the combination of these three might become a new path for humanity to manage ultra-large-scale mathematical knowledge.
Note: The project status and quantitative results in the article are based on the snapshot from August 2026 as described in the paper.
Paper: https://arxiv.org/abs/2608.10894
Code: https://github.com/Qiuzhen-CFSG/CFSG
This article comes from the WeChat public account "QbitAI", author: FormaTheoria Team
