In 7 Months, a Tsinghua-Led AI Team Formalized Landmark Group Theory Proofs in Lean, Matching a 6-Year Human Effort

Forum topic · 小凯 · 2026-09-01

Summary

FormaTheoria, a project initiated by Shing-Tung Yau and led by students from Tsinghua University's Qiuzhen College with support from the Yau Mathematical Sciences Center, the Institute for AI Industry Research, and the University of Warwick, is formalizing the Classification of Finite Simple Groups (CFSG) with AI and the Lean proof assistant. Starting January 22, 2026, the team completed in seven months a chain of four landmark theorems: Feit–Thompson Odd Order Theorem, Glauberman Z* Theorem, Brauer–Suzuki Theorem, and Bender–Suzuki Theorem. The Feit–Thompson theorem alone previously took a ~15-person team six years to formalize in Rocq. The resulting snapshot includes 994,000+ lines of Lean code across 850+ files, drawing on 15 books and papers (1,037 pages, about 65.6% discovered during the proof process), with 30,298 declarations, 186,187 dependencies, and a 458-level deepest dependency chain. The system also uncovered four classes of hidden issues in the original literature, including inconsistent definitions, a missing odd-order hypothesis in a Peterfalvi lemma, typographical errors, and a misplaced divisibility condition. The full CFSG formalization remains incomplete, but the project demonstrates AI rebuilding century-scale mathematical proofs into verifiable, auditable, reusable infrastructure.

FormaTheoria: Formalizing the Classification of Finite Simple Groups with AI and Lean

When a mathematical proof spans hundreds of papers over decades and nearly 20,000 pages, whether it is actually correct can no longer be verified by any single referee in a few weeks. FormaTheoria, a project pushed forward by Fields Medalist and foreign member of the Chinese Academy of Sciences Shing-Tung Yau, hands this verification work to AI and the Lean proof assistant. As of August 2026, the project had covered in 7 months ground that took a human team 6 years.

Turning Mathematical Proofs into Clickable Code

The Classification of Finite Simple Groups (CFSG) is a pillar of modern group theory. Its proof was completed by hundreds of mathematicians over decades, scattered across hundreds of papers and monographs totaling nearly 20,000 pages — a giant proof no one can fully reread from start to finish.

Yet CFSG is foundational infrastructure for nearly every theorem that depends on finite symmetry structures: distance-transitive graphs, the Frobenius conjecture, permutation group algorithms, subgroup growth, field extensions, Riemann surface covers, Waring-type problems in group theory, expander graphs and approximate groups, and more. The 1994 Fields Medal awarded to Efim Zelmanov for the restricted Burnside problem rested on this foundation.

Infrastructure of this kind cannot have hidden defects — if CFSG were wrong, everything built on it would need re-examination. One significant gap in the classification proof was only filled more than twenty years later by a two-volume, 1,220-page monograph. This state of multi-generational relay, with inconsistent symbols and definitions across sources, is exactly where AI can intervene.

FormaTheoria: A Continuously Updated Proof Map

On January 22, 2026, FormaTheoria made its first code submission. The effort is led by students of Tsinghua University's Qiuzhen College, working with the Yau Mathematical Sciences Center, the Institute for AI Industry Research (AIR), and the University of Warwick. The goal: let AI start from original mathematical literature, automatically trace dependencies, integrate knowledge, and construct formal proofs, then verify them in Lean.

CFSG is not a ready-made problem set. It is a pile of literature with nested citations and definitions — and there is no way to know in advance how many obstacles lie on the path. The project initially listed only 3 primary sources; 12 more emerged as the proof progressed. In total, the project consulted 15 books and papers (1,037 pages), of which about 65.6% of the pages were discovered gradually during the proof process.

Faced with these surprise dependencies, FormaTheoria did something simple: whenever a prerequisite theorem was missing, it paused the current proof, filled in the dependency, added it to the knowledge base, and then resumed. Already-verified results are reused rather than recomputed.

The system also implements three key safeguards:

Dependency-aware parallelism: independent tasks run in parallel; tasks needing the same prerequisite compute it only once; shared mathematical content is modified serially. Controlled experiments showed a 4.2× speedup on test tasks.
Translation vs. review separation: a translation component writes Lean statements; a review component checks them against the source item by item. Across 14 literature sections analyzed, 11 first-pass translations were sent back for revision.
Failure-path archiving: failed proof routes are recorded rather than deleted, so the system avoids repeatedly entering the same dead end.

Seven Months, Four Key Theorems, 994,000+ Lines of Code

By August 2, 2026, the project had completed a key theoretical chain ending at the Bender–Suzuki theorem, successively formalizing:

1. Feit–Thompson Odd Order Theorem 2. **Glauberman Z* Theorem 3. Brauer–Suzuki Theorem 4. Bender–Suzuki Theorem

Each of these builds on the vast mathematical groundwork laid by the previous one. A snapshot at completion:

| Dimension | Value | |---|---| | Lines of Lean code | 994,000+ | | Code files | 850+ | | Literature consulted | 15 works / 1,037 pages | | Bender–Suzuki network declarations | 30,298 | | Dependencies | 186,187 | | Longest dependency chain | 458 levels | | Total declarations incl. Lean's libraries | 74,922 | | Total dependencies incl. libraries | 1,440,000+ | | Longest single agent run | 9.17 days | | Compaction/cleanup operations | 606 |

For perspective: the previous Rocq formalization of Feit–Thompson took roughly 15 people six years. FormaTheoria completed equivalent work in 7 months and extended it to three more key theorems.

Machines Don't "Fill in the Blanks" — So It Found 4 Hidden Defects

Math papers assume readers know the context, so authors omit already-stated conditions or treat equivalences between definitions as common knowledge. Human referees mentally fill in these gaps; Lean does not.

This rigor let FormaTheoria surface four classes of hidden issues in the original literature:

Inconsistent definitions across sources: the definition of "type I maximal subgroups" differed formally between two sources ("every complement exists" vs. "a complement exists"). The system used the Schur–Zassenhaus theorem to prove they are equivalent in the CFSG context, bridging the two sources.

Missing hypotheses: a Peterfalvi lemma omitted the premise that the group has odd order; since the proof kept using it, the system traced usages back and added the condition to the statement automatically.

Typographical errors in subscripts/objects: in Higman's proof, a range from u₀ to uₘ should have been u₀ to uₘ₋₁; the system identified and corrected it.

Misplaced divisibility conditions: in a theorem of Huppert, the condition that a divisor d divides something was placed incorrectly; after the system found a counterexample, it was escalated to humans.

The counterintuitive lesson: machine verification of large mathematical projects contributes not only "is the proof correct" but also "does the original text contain errors" — converting details readers fill in from experience into clickable, traceable mathematical justification.

The Road Not Yet Finished

FormaTheoria has completed four theorems on CFSG's critical path. The full classification theorem itself remains unformalized, and there is a long way to go. But the direction is clear: AI is no longer just "solving prepared math problems" — it is entering the literature jungle, crossing decades, authors, and notation systems, to rebuild a verifiable, traceable, extensible mathematical infrastructure layer by layer.

Once extended, this infrastructure offers three core capabilities:

Reusable: verified definitions, lemmas, and proofs become knowledge modules callable by later research.

Auditable: every step of reasoning corresponds to a line of Lean code; every fix corresponds to a passage of source text.

Sustainable: multiple theorems share one theoretical framework; new theorems only require filling in dependencies, not rewriting foundations.

The FormaTheoria team envisions a human–AI collaboration model for the AI era: humans decide which problems to pursue and where key judgments lie; AI handles large-scale search and derivation; formal systems ensure every accepted step can be re-checked.

> Side note — What is Lean?** An interactive theorem-proving language created by Leonardo de Moura at Microsoft Research in 2013, which writes mathematical arguments as code a computer can verify step by step. By late 2025, its community math library Mathlib contained over 250,000 theorems and 120,000 definitions; in 2025 it received the ACM SIGPLAN Programming Languages Software Award and the Skolem Award.

The real bet of this path is not whether AI can write proofs, but whether AI can make a century-scale proof clickable. If it succeeds, CFSG will no longer be a row of hardcovers in a library, but a network that new theorems can call in reverse and trace forward.

Sources

FormaTheoria team report (Fanpu / Tencent News, 2026-08-31): https://news.qq.com/rain/a/20260831A04WXM00
FormaTheoria project paper: arXiv:2608.10894 (August snapshot)
Code repository: https://github.com/Qiuzhen-CFSG/CFSG
Stephen D. Smith, *Applying the Classification of Finite Simple Groups: A User's Guide*, AMS, 2018 (231 pages / 10 chapters / 14 application topics)
Chris Hsu, "How One Programming Language Rewrote Mathematics and Why Software Is Next," IBTimes / Web Pulse, 2026