Key points
- Project: FormaTheoria, championed by Shing-Tung Yau, made its first code commit on January 22, 2026. The lead team consists of students from Tsinghua University's Qiuzhen College, working with the Yau Mathematical Sciences Center, the Institute for AI Industry Research (Tsinghua), and the University of Warwick. Goal: have AI automatically extract dependencies from raw mathematical literature, build a knowledge base, construct formal proofs, and have the Lean proof assistant verify them.
- Target: The Classification of Finite Simple Groups (CFSG) — a proof spanning hundreds of papers and nearly 20,000 pages, built by generations of mathematicians. CFSG is foundational infrastructure for results on distance-transitive graphs, Frobenius conjectures, expanders and approximate groups, and more (e.g., Efim Zelmanov's 1994 Fields Medal work on the restricted Burnside problem).
- Dependency-aware parallelism: independent tasks run in parallel; shared prerequisites are computed once; globally shared mathematical content is modified serially. Controlled experiments showed a 4.2x speedup on test tasks.
- Translation vs. audit separation: a translation component writes Lean statements; a separate audit component checks them item-by-item against the source. Of 14 analyzed literature sections, 11 required first-round rework.
- Failure archival: failed proof paths are recorded, preventing the system from repeatedly entering the same dead ends.
- FormaTheoria team report (Fanpu / Tencent News, 2026-08-31): https://news.qq.com/rain/a/20260831A04WXM00
- Project paper: arXiv:2608.10894
- Code repository: https://github.com/Qiuzhen-CFSG/CFSG
- Stephen D. Smith, *Applying the Classification of Finite Simple Groups: A User's Guide*, AMS, 2018
Results by August 2, 2026
The project completed a chain of four theorems leading toward the Bender–Suzuki Theorem:
1. Feit–Thompson Odd Order Theorem 2. Glauberman Z* Theorem 3. Brauer–Suzuki Theorem 4. Bender–Suzuki Theorem
Snapshot metrics:
| Metric | Value | |---|---| | Lines of Lean code | 994,000+ | | Code files | 850+ | | Literature consulted | 15 books/papers, 1,037 pages | | Declarations in the Bender–Suzuki network | 30,298 | | Dependency edges | 186,187 | | Longest dependency chain | 458 levels | | Total declarations incl. Mathlib | 74,922 | | Total dependencies incl. libraries | 1,440,000+ | | Longest single agent run | 9.17 days | | Compaction/consolidation events | 606 |
For comparison, the earlier Rocq formalization of Feit–Thompson alone took roughly 15 people six years. FormaTheoria completed equivalent work in 7 months and extended it to three more theorems.
Notably, about 65.6% of the 1,037 pages consulted were discovered only during the proof process — the project started with just 3 sources and uncovered 12 more as hidden dependencies emerged.
System architecture and safeguards
When a prerequisite theorem is missing, the system pauses, formalizes the dependency into the knowledge base, then resumes the main proof.
Four defects uncovered in the original literature
Because Lean does not "fill in" context the way human readers do, formalization exposed four classes of hidden problems:
1. Inconsistent definitions across sources: two references defined "type I maximal subgroups" non-equivalently ("every complement" vs. "some complement"). The system used the Schur–Zassenhaus theorem to prove their equivalence in the CFSG context, bridging the sources. 2. Omitted hypotheses: a Peterfalvi lemma omitted the "group has odd order" premise. The system traced its usage and added the condition to the statement automatically. 3. Typographical/indexing errors: in Higman's proof, a sequence running from u₀ to u_m should have been u₀ to u_{m−1}; the system identified and corrected it. 4. Misplaced divisibility condition: in a theorem of Huppert, a divisibility condition on a factor d was misplaced; after finding a counterexample, the system escalated to humans.
These cases show that machine verification adds value beyond "is the proof correct" — it also checks "is the source text itself correct."
What remains
The full CFSG formalization is not complete; the project has finished four key theorems on the critical path. But the direction is established: reusable, auditable, extensible mathematical infrastructure, with humans choosing problems and making key judgments, AI performing large-scale search and derivation, and formal systems guaranteeing every accepted step is re-checkable.
> Side note — What is Lean? An interactive theorem-proving language created by Leonardo de Moura at Microsoft Research in 2013. By 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.