When a mathematical proof is scattered across hundreds of papers spanning decades — nearly 20,000 pages in total — whether that proof actually holds can no longer be verified by any single reviewer in a few weeks. The FormaTheoria project, championed by Shing-Tung Yau (foreign member of the Chinese Academy of Sciences), entrusts this verification work to AI and the Lean proof assistant. As of August 2026, the project had completed in 7 months what took a human team 6 years to formalize.
Turning a 'Mathematical Proof' into 'Clickable Code'
At any gathering mathematicians must attend, the Classification of Finite Simple Groups (CFSG) is the host. Its proof was completed by more than a hundred mathematicians over decades, spread across hundreds of papers and monographs totaling nearly 20,000 pages — a mega-proof 'no one can ever fully re-read from start to finish.'
Yet CFSG is the underlying infrastructure for almost every theorem that depends on 'finite symmetry structures': 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... Important results in all these areas call back to CFSG. The 1994 Fields Medal awarded to Efim Zelmanov was precisely because he reached the CFSG stepping stone in his work on the restricted Burnside problem.
Since CFSG is infrastructure, it cannot harbor hidden defects. If it were wrong, everything built on it would need re-examination. But the proof is old — one significant gap in the classification proof was only filled more than twenty years later, by a two-volume monograph running 1,220 pages.
This state of 'a relay across generations, with symbols and definitions each doing their own thing' is exactly where AI can intervene.
FormaTheoria: A Continuously Updated 'Proof Map'
On January 22, 2026, FormaTheoria made its first commit. The core team consists of students from Tsinghua University's Qiuzhen College Qiuzhen-led program, working with the Yau Mathematical Sciences Center, the Institute for AI Industry Research (Tsinghua), and the University of Warwick. Their goal is direct: let AI start from the original mathematical literature, automatically trace dependencies, integrate knowledge, and construct formalized proofs, then hand them to the Lean proof assistant for verification.
But CFSG is not a pre-written LeetCode problem set. It is a pile of scattered literature with nested citations and definitions — you never know how many mountains lie along the road.
The project initially listed only 3 main sources; as the proof progressed, 12 more sources emerged, and the project ultimately consulted 15 books and papers totaling 1,037 pages — about 65.6% of those pages were discovered along the way.
Facing this 'blind-box' dependency structure, 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 returned to the original task. Verified results are reused repeatedly and never recomputed.
It also built in three key safeguards:
- Dependency-aware parallelism: independent tasks run in parallel; tasks sharing the same prerequisite compute it only once; shared mathematical content with far-reaching effects is modified serially. Controlled experiments showed this scheduling achieved a 4.2× speedup on test tasks.
- Translation vs. review separation: the translation component writes Lean statements; the review component checks each one against the original text. Of 14 literature sections analyzed in the paper, 11 first-round translations were sent back for revision.
- Failure-path archiving: failed proof routes are not deleted but recorded, preventing the system from repeatedly walking into the same dead end.
- Inconsistent definitions across sources: e.g., the 'type I maximal subgroup' definition — one source says 'for every complement structure,' another 'there exists a complement structure.' The system bridged them via the Schur–Zassenhaus Theorem, proving the two formulations equivalent in the CFSG context.
- Missing hypotheses in theorem statements: e.g., a Peterfalvi lemma omitted the 'the group has odd order' premise. The proof kept using it; since Lean doesn't auto-supply background, the system traced usage sites back and added the condition to the statement.
- Typographical errors in subscripts/objects: e.g., in Higman's proof, a range from u₀ to uₘ should read u₀ to uₘ₋₁ — automatically identified and corrected.
- Misplaced divisibility conditions: e.g., in a theorem of Huppert, a divisibility condition on factor d was misplaced — the system found a counterexample and escalated to humans.
- Reusable: verified definitions, lemmas, and proofs become knowledge modules that future research can call directly, without rebuilding from scratch.
- Auditable: every inference step corresponds to a line of Lean code; every fix corresponds to a passage of original text.
- Sustainable: multiple theorems share one theoretical framework; new theorems only require filling in dependencies, not rewriting foundations.
- FormaTheoria team, 'In 7 months surpassing 15 mathematicians' 6 years of work, AI writes a million lines of code to verify a mega mathematical proof project', Tencent News (返朴 reprint), 2026-08-31, https://news.qq.com/rain/a/20260831A04WXM00
- FormaTheoria project paper, arXiv:2608.10894 (August project snapshot)
- Project 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
Seven Months, Four Key Theorems, 994,000 Lines of Code
By August 2, 2026, the project had completed a theoretical chain extending to the Bender–Suzuki Theorem, successively proving:
1. Feit–Thompson Odd Order Theorem 2. **Glauberman Z* Theorem 3. Brauer–Suzuki Theorem 4. Bender–Suzuki Theorem
These four theorems are linked, with each proof building on the vast mathematical foundation laid by the previous one.
Snapshot at completion:
| Dimension | Value | |---|---| | Lines of Lean code | 994,000+ | | Code files | 850+ | | Literature consulted | 15 works / 1,037 pages | | Declarations in Bender–Suzuki network | 30,298 | | Dependencies | 186,187 | | Longest dependency chain | 458 layers | | Total declarations (incl. Lean core libs) | 74,922 | | Total dependencies (incl. core libs) | 1,440,000+ | | Longest single agent run | 9.17 days | | Cumulative compaction/consolidation passes | 606 |
The comparison is stark: the earlier Rocq formalization of Feit–Thompson was completed by roughly 15 people over six years. FormaTheoria matched that work in 7 months and extended it to three more key theorems. For AI this is an ultra-long-horizon task; for a human team it saves six years.
Machines Don't 'Fill in the Blanks' — So It Found 4 Hidden Defects
Mathematical papers assume readers know the context, so authors omit previously stated conditions or treat equivalences between definitions as common knowledge. Human reviewers' brains automatically fill in this background — but Lean does not.
This obsessive refusal to fill in gaps led FormaTheoria to uncover four classes of hidden issues in the original literature during formalization:
These cases reveal a counterintuitive truth: the value of machine verification for large mathematical projects is not only 'is the proof correct' but also 'are there errors in the original text.' Converting details readers previously filled in from experience into clickable, traceable mathematical grounding is the second layer of what formalization contributes.
The Road Still Ahead
FormaTheoria has so far completed four theorems on the critical path of CFSG. The full classification theorem itself remains unformalized — there is still a considerable distance to the finish line.
But the direction is clear: AI is no longer just 'solving pre-prepared math problems' — it is entering the literature jungle, crossing different eras, authors, and notation systems, layer by layer rebuilding a verifiable, traceable, extensible mathematical infrastructure.
Once scaled, this infrastructure offers three core capabilities:
The FormaTheoria team envisions a human-AI collaboration model for the AI era: humans decide 'which problems to choose and where key judgments lie,' AI handles 'large-scale search and derivation,' and formal systems ensure 'every accepted step can be re-verified.'
> Tip | What is Lean? An interactive theorem-proving language created by Leonardo de Moura at Microsoft Research in 2013, which turns mathematical arguments into code a computer can verify step by step. As of late 2025, its community math library Mathlib contained over 250,000 theorems and 120,000 definitions, and in 2025 received the ACM SIGPLAN Programming Languages Software Award and the Skolem Award.
When a proof grows too large for any individual to review from scratch, this tripartite combination may become a new path for humanity to manage ultra-large-scale mathematical knowledge.
> Observation: the real bet on this path is not 'can AI write proofs' but 'can AI make a century-scale proof clickable.'** If it succeeds, CFSG will no longer be a row of gray hardcovers in a library, but a network that new theorems can call into and trace backward through.