Over more than 7 months, AI has completed the workload equivalent to that of more than 15 mathematicians working for 6 years, writing millions of lines of code to challenge the engineering of verifying extra-large mathematical proofs.
Classification of Finite Simple Groups (CFSG) is widely recognized as one of the largest-scale proof projects in modern mathematics.
This proof was completed by hundreds of mathematicians through decades of continuous collaborative efforts, with its results scattered across hundreds of papers and monographs, totaling nearly 20,000 pages in length. Its scale has far exceeded the boundary that a single person or even a single team can fully review.
Against this backdrop, introducing AI assistance to carry out large-scale formal verification has become a new path that must be attempted.
To promote the development of AI for Math, under the advocacy of Mr. Shing-Tung Yau, students from the Leading Talent Program of Qiuzhen College, Tsinghua University, and research teams from Yau Mathematical Sciences Center, Institute for Intelligent Industry Research and the University of Warwick proposed FormaTheoria — Artificial Intelligence Assisted Workflow for Mathematical Research: it enables AI to start from original mathematical literature, automatically sort out dependency relationships, integrate knowledge systems and construct formal proofs, and finally submit them to the Lean proof assistant for step-by-step verification.
As of August 2026, FormaTheoria has completed Lean formalization of four key theorems, producing more than 994,000 lines of interrelated coded mathematical theories. Although there is still a long way to go to fully verify the Classification of Finite Simple Groups, this achievement has become an important milestone on the way to this ultimate goal.
CFSG provides the underlying system for a large number of important mathematical results
"Classification of Finite Simple Groups" sounds very abstract. In layman's terms, it is like a "basic parts list" for finite symmetries: any complex finite symmetric structure can be disassembled layer by layer, and finally a number of basic units that cannot be further split are obtained; the role of CFSG is to tell mathematicians exactly what these basic units are.
Usually, mathematical research will first split a complex problem into these basic units, and then process them category by category according to the complete list provided by CFSG. Therefore, CFSG has become an infrastructure that other proofs can call at any time. If this set of "infrastructure" hides loopholes, a large number of subsequent results built on its relevant conclusions may be affected.
Some professional reviews provide quantitative proof for the application of GFSG. In 2018, the American Mathematical Society specially published Stephen D. Smith's monograph "Applying the Classification of Finite Simple Groups: A User's Guide". The book has 231 pages, 10 chapters in total, which sorts out the application scenarios of GFSG. The public catalogue of the last two chapters of the book lists 14 numbered application topics, including distance-transitive graphs, Frobenius conjecture, permutation group algorithms, subgroup growth of finitely generated groups, field extension, Riemann surface covering, Waring's problem in group theory, expander graphs and approximate groups, etc.
The application value of GFSG has also been recognized at the highest level of the international mathematics community. In 2014, the International Congress of Mathematicians invited Robert Guralnick, winner of the 2018 Cole Prize in Algebra of the American Mathematical Society, to give a special report titled "Applications of the Classification of Finite Simple Groups".
These applications include important results with great academic influence. CFSG is a key link in the complete proof chain of the restricted Burnside problem, and Efim Zelmanov won the Fields Medal in 1994 for solving this problem. Smith's monograph also lists the Waring's problem on finite simple groups and expander graphs as important application directions of CFSG, and relevant representative papers are published in "Annals of Mathematics" (Waring's problem; diameters of finite simple groups and their applications). These examples show that CFSG has supported a series of important works that have won top academic awards and been published in top mathematical journals.
In this sense, CFSG has become a set of underlying systems that have been used repeatedly. As more and more downstream results accumulate, verifying its correctness and auditability becomes increasingly critical. Traceable and repeatable machine verification of CFSG has significance beyond group theory itself.
However, the difficulty lies in that the proofs of this underlying system come from different eras, different authors and different literatures, and the symbols, definitions and default conditions used are often inconsistent, and a citation may even point to another complete set of literatures. Historically, an important gap in the classification proof was not filled until more than 20 years later by a two-volume monograph of up to 1220 pages. FormaTheoria not only needs to verify the step-by-step reasoning gradually, but also check whether the definitions, conditions and citations among hundreds of literatures can be fully connected, and finally form a proof chain without breaks.
How AI advances ultra-large-scale proof projects
Many AI mathematics systems face a pre-prepared problem, including all ready-made problems, definitions and tools, and AI is only responsible for finding the proof. But FormaTheoria is different. It needs to reconstruct the mathematical foundation behind the problem from a large number of scattered literatures first, and then complete the proof. This work mainly faces four difficulties:
First, the system does not know in advance how much material needs to be consulted.
A citation may lead to another paper, which in turn leads to more pre-work. The project initially had only 3 main sources, and 12 more sources were discovered during the proof process; the later supplemented materials accounted for 65.6% of all consulted pages. The processing method of FormaTheoria is: once it finds that a precondition theorem is missing, it will pause the current proof, find and formalize this dependency, and then return to the original task to continue advancing. The verified results will be stored in a unified knowledge base for repeated calls in subsequent proofs.
Second, it is difficult to directly splice different literatures.
Different authors use different definitions, symbols and default conditions. Two definitions may be completely equivalent mathematically, but once written into Lean code, they may be incompatible. FormaTheoria will repeatedly compare the original text with the existing code to build the necessary transformation relationships. At the same time, the system will protect the verified mathematical statements, and check whether each repair will affect subsequent proofs. In this way, multiple independent works and papers can be gradually integrated into the same theoretical framework.
Third, the code that passes the check may still misunderstand the original text.
Lean is only responsible for checking whether the proof logic is self-consistent and whether the conclusion is derived from the premise, but cannot judge whether this conclusion is faithful to the original text. AI is very likely to miss a certain condition, confuse "for all" and "there exists", or even incorrectly modify the conclusion. To this end, FormaTheoria has specially set up an independent review checkpoint: the translation component first writes the Lean statement, and the review component checks item by item against the original text. Among the 14 literature sections analyzed in the paper, the first-round translations of 11 sections were returned for modification. This independent review mechanism thus becomes the second "insurance" beyond machine verification.
Fourth, the original literature itself may also have problems.
Old literatures may have typographical errors, missing conditions or ambiguous expressions. FormaTheoria will retain the original page for retrospective investigation when subsequent proofs encounter contradictions. If the literature can support correction, the system will supplement conditions or establish compatibility relationships; when the evidence is insufficient, the system will record the problem and hand it over to mathematics professionals for judgment.
In addition, this project also requires AI to maintain its rhythm over a long period of time. A single conversation cannot accommodate the complete task. To this end, FormaTheoria uses a continuously updated "proof map" to manage progress: the more arduous goals are split into smaller auxiliary theorems, successful results are fed back to the main theorem layer by layer, and failed routes are also recorded to avoid the system from repeatedly entering the same dead end.
In terms of parallel strategy, the project also has a special design. Mutually independent tasks can be advanced at the same time; when multiple tasks encounter the same pre-result, the system only completes it once and allows other tasks to reuse it. Those public mathematical contents that may affect the whole body due to a slight move are modified one by one in sequence to avoid conflicts. The controlled experiment in the paper shows that this dependency-aware parallel method achieves a 4.2x speedup on the tested tasks.
Thus, FormaTheoria forms a complete workflow: search for literatures, supplement dependencies, translate original texts, construct proofs, perform machine verification, conduct independent reviews, coordinate conflicts, and hand over uncertain problems to mathematics professionals. Each step has clear responsibilities and traceable records. This is exactly the design made to solve the practical difficulties in ultra-large-scale proof projects, enabling AI to gradually connect scattered mathematical literatures into a verifiable, traceable and sustainably expandable theoretical system.
△
Seven months, four key theorems, nearly one million lines of verifiable code
From the first code submission of FormaTheoria on January 22, 2026 to August 2, 2026, the project has opened up a key theoretical chain extending to the Bender–Suzuki Theorem, and successively completed the proofs of the Feit–Thompson Odd Order Theorem, Glauberman Z* Theorem and Brauer–Suzuki Theorem.
These four theorems are not isolated from each other. They form an interconnected and important route in the Classification of Finite Simple Groups, and the proof of the latter theorem is often built on the huge mathematical foundation laid by the former.
The project snapshot when the above proofs were completed includes:
- More than 994,000 lines of Lean code;
- More than 850 code files;
- The system has consulted a total of 15 books and papers, totaling 1037 pages, about two-thirds of which were gradually discovered during the advancement of the proof.
Of course, the number of lines of code can only show one side of the project scale. If we take the Bender–Suzuki Theorem as the end point to trace back, the project has formed a proof network containing 30,298 mathematical statements and 186,187 dependency relationships, with the longest dependency chain reaching 458 layers. If the relevant content in the Lean base library is also included, this network will expand to 74,922 statements and more than 1.44 million dependency relationships. It can be said that behind nearly one million lines of code is a deeply intertwined and closely linked proof network. This study shows that AI agents can already continuously promote large-scale, ultra-long-distance mathematical projects under the combined effect of machine verification and hierarchical review.
The actual operation process of the project also has the characteristics of ultra-long duration. The longest single agent execution recorded in the paper lasted for 9.17 days, during which the system performed 606 times of compression and sorting on the accumulated information, while always retaining the current proof goals, completed results, and problems to be solved. These data show that the project manages an evolving ultra-long proof network, which cannot be covered by a single generation or a single conversation at all.
In the past, large-scale mathematical formalization could only highly rely on manual input, usually requiring multiple researchers to collaborate continuously for several years. A comparable historical reference: the previous Rocq formalization version of the Feit–Thompson Theorem was completed by about 15 people after six years of work. However, FormaTheoria completed all the content of this manual project in seven months, and further expanded to the formalization of other key theorems. Seven months is still an extremely long running cycle for an AI agent task, but compared with the traditional manual formalization, the intervention of AI has significantly shortened the time scale of project operation.
△
Formalization makes the hidden problems in the literature emerge one by one
Mathematical literature is usually oriented to researchers who are familiar with this field. Therefore, authors often omit conditions that have appeared in the previous text, or default that readers can identify the equivalence relationship between different definitions. Some small typographical errors or symbol errors are often naturally ignored or corrected when read manually. But FormaTheoria works differently: when it translates the literature into Lean code line by line, every definition, every condition and every step of reasoning must be written clearly and unambiguously. It is this strict requirement of line-by-line verification that makes the originally invisible problems in the original literature obvious.
The paper records in detail various literature problems discovered by the project, including inconsistent definitions of the same concept in different materials, missing necessary conditions in theorem statements, wrong positions of divisibility conditions, and even errors in subscripts in proofs. Some of these problems can be automatically corrected according to the context of the literature; problems with insufficient evidence will be handed over to mathematicians for further judgment.
A typical case comes from two materials about the Odd Order Theorem. Both materials define "type I maximal subgroups", but the difference is that one requires a certain property to hold for "every complementary structure", while the other only requires "there exists a complementary structure" to satisfy this property. Formally, the former is obviously stronger than the latter, so the two sets of definitions cannot be directly connected. FormaTheoria keenly identified this difference during the formalization process, and then proved that the two definitions are actually equivalent here with the help of the Schur–Zassenhaus Theorem, thus successfully building a bridge connecting the two literatures.
Another case comes from a lemma of Peterfalvi. The formal statement of this lemma omits the prerequisite that "the order of a certain group is odd", but the subsequent proof is actually inseparable from this condition. Although when applying this lemma later, the previous text has guaranteed this condition, and the overall argument was not interrupted, Lean will not automatically supplement this background information. After tracking the proof path and usage positions of this lemma, FormaTheoria automatically explicitly 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 wrote the object H that should have appeared as M, and the two reference materials retained the same error. A theorem of Huppert put the factor d into the wrong divisibility condition; the system found a counterexample and terminated the proof, and handed the problem over to mathematicians for verification. Manual confirmation confirmed the correct condition. A proof segment of Higman also numbered a set of basis vectors from u₀ to uₘ, and the correct range should be to uₘ₋₁; this subscript error was automatically identified and corrected by the system during the proof process.
These cases reflect another important value of machine verification for large-scale mathematical projects. While constructing formal proofs, FormaTheoria also conducts fine-grained review of the original literature: it records where the problem appears, what conditions are required for subsequent proofs, which literatures the modification basis comes from, and whether the modification will affect other results. For CFSG, which is composed of hundreds of interconnected materials, this traceable review mechanism can convert those details that used to be supplemented by readers' experience into clearly verifiable mathematical basis.
Future Outlook
FormaTheoria has not yet completed the overall formalization of the Classification of Finite Simple Groups, and there is still a long way to go to reach the final goal. The project is accelerating its advancement, continuously moving towards the complete formalization of one of the largest-scale proof projects in modern mathematics. Existing results show that AI has been able to maintain and expand large-scale mathematical environments within a few months, track complex dependency relationships across multiple literatures, and build interconnected and objectively large theoretical systems under strict verification. The capability boundary of