7 个月跑赢 6 年：清华团队把有限单群分类「钉」进了 Lean
当一个数学证明散落在数百篇论文、跨度数十年、字面量接近两万页时，「证明是否真的成立」这件事，就不再是某一位审稿人能用几周时间核对清楚的了。中国科学院外籍院士丘成桐推动的 FormaTheoria 项目，把这套核验工作交给了 AI 与 Lean 证明助手。2026 年 8 月，项目已经用 7 个月时间走完了人工团队 6…
当一个数学证明散落在数百篇论文、跨度数十年、字面量接近两万页时，「证明是否真的成立」这件事，就不再是某一位审稿人能用几周时间核对清楚的了。中国科学院外籍院士丘成桐推动的 FormaTheoria 项目，把这套核验工作交给了 AI 与 Lean 证明助手。2026 年 8 月，项目已经用 7 个月时间走完了人工团队 6 年的形式化之路。
🪛 把「数学证明」变成「可点击的代码」
在一场数学家必须出席的舞会上，有限单群分类定理（Classification of Finite Simple Groups，下文简称 CFSG） 是主持人。它的证明由上百位数学家接力数十年完成，结论散落在几百篇论文和专著里，全本加起来接近 20000 页——这是一套「没人能从头到尾完整重读一遍」的巨型证明。
但 CFSG 又是几乎所有依赖「有限对称结构」的数学定理的底层设施：距离传递图、Frobenius 猜想、置换群算法、有限生成群的子群增长、域扩张、黎曼曲面覆盖、群论中的 Waring 问题、扩展图与近似群……这些方向里重要结论的证明，都会回头调用 CFSG。1994 年菲尔兹奖颁给 Efim Zelmanov，正是因为他在受限 Burnside 问题上走到了 CFSG 这块跳板上。
CFSG 既然是基础设施，就不能有暗病。一旦错了，建在它头上的成果都得重审。但它实在太老了——分类证明中有一处重要缺口，直到二十多年后，才由两卷、多达 1220 页的专著补齐。
这种「几代人的接力，符号与定义各管各的」状态，正是 AI 介入的最佳切点。
🧠 FormaTheoria：一张持续更新的「证明地图」
2026 年 1 月 22 日，FormaTheoria 第一次提交代码。牵头团队是清华大学求真书院领军班学生，配合丘成桐数学科学中心、智能产业研究院和华威大学。他们的目标很直接：让 AI 从原始数学文献出发，自动梳理依赖关系、整合知识体系并构造形式化证明，再交给 Lean 证明助手核验。
但 CFSG 不是一个写好的 LeetCode 题库。它是一堆零散的文献，引用与定义彼此嵌套，你根本不知道这条路要翻多少座山。
项目最初只列了 3 个主要来源，证明推进过程中又陆续冒出 12 个来源，最终整个项目查阅了 15 部书籍与论文、共 1037 页，其中约 65.6% 的页码是在证明过程中逐步发现的。
面对这种「盲盒式依赖」，FormaTheoria 做了一件朴素的事：一旦发现缺一个前置定理，就暂停当前证明，把这个依赖补齐并写进知识库，然后再回到原任务继续推进。已经核验的成果则被反复调取，不会重复计算。
它同时设计了三条关键防线：
- 依赖感知并行：相互独立的任务并行推进；多个任务若需要同一前置结果，只算一次；牵一发动全身的公共数学内容则串行修改。对照实验显示，这种调度方式在测试任务上实现了 4.2 倍加速。
- 翻译 vs 审查分离：翻译组件写 Lean 陈述，审查组件对照原文逐项核对。在论文分析的 14 个文献小节中，11 节的首轮翻译被打回修改。
- 失败路径存档：失败的证明路线不会被删除，而是被记录下来，避免系统反复走进同一条死胡同。
📊 七个月，四个关键定理，99.4 万行代码
到 2026 年 8 月 2 日，项目已经打通一条延伸到 Bender–Suzuki 定理的关键理论链条，途中依次完成了：
1. Feit–Thompson 奇数阶定理 2. **Glauberman Z* 定理 3. Brauer–Suzuki 定理 4. Bender–Suzuki 定理
这四个定理彼此衔接，后一个证明往往建立在前一个铺下的庞大数学基础之上。
完工时快照如下：
| 维度 | 数值 |
|---|---|
| Lean 代码行数 | 994,000+ |
| 代码文件数 | 850+ |
| 已查阅文献 | 15 部 / 1037 页 |
| Bender–Suzuki 网络声明 | 30,298 |
| 依赖关系 | 186,187 |
| 最长依赖链 | 458 层 |
| 含 Lean 基础库后总声明 | 74,922 |
| 含基础库后总依赖 | 1,440,000+ |
| 最长单次智能体执行 | 9.17 天 |
| 期间累计压缩整理 | 606 次 |
🔍 机器不会「脑补」，所以它找出了 4 处暗病
数学论文默认读者熟悉上下文，所以作者会省略已出现过的条件、把不同定义的等价性当作共识。人类审稿时大脑会自动脑补这些「背景信息」，但 Lean 不会。
正是这种「不脑补」的强迫症，让 FormaTheoria 在形式化过程中挖出了原始文献里四类隐藏问题：
其中最值得一提的是「类型 I 极大子群」的定义冲突：两部资料对同一概念给出了形式上不等价的写法，看起来前者更强；系统识别后调用 Schur–Zassenhaus 定理，证明两者在 CFSG 的语境里实际等价，从而把两部文献搭上了桥。
另一处 Peterfalvi 引理遗漏了「群的阶为奇数」这一前提。证明时实际一直在用它，Lean 不会自动补背景，于是系统沿着使用位置倒查，主动把条件加进了定理陈述。
这些案例透露了一个反直觉的事实：
机器核验对大型数学工程的价值，不止「证明对不对」，还包括「原文有没有写错」。 把读者凭经验补全的细节，转化为可点击、可追溯的数学依据，正是形式化能贡献的第二层东西。🧭 仍未走完的路
FormaTheoria 目前完成的是 CFSG 关键路径上的四个定理。完整分类定理本身仍未被形式化，距离终点还有相当距离。
但项目展示的方向已经清楚：AI 不再只是「解已经准备好的数学题」，而是
进入文献丛林，跨越不同年代、不同作者、不同符号系统，逐层重建一套可核验、可追溯、可扩展的数学基础设施。这套设施一旦扩展，将具备三条核心能力：
当一项证明庞大到任何个人都难以从头复核时，这三者的结合，或许会成为人类管理超大规模数学知识的一条新路径。
观察：这条路径的真正赌注不在于「AI 能不能写证明」，而在于「AI 能不能让一个世纪级证明变得可点击」。 如果成功，CFSG 将不再是图书馆里的一排灰皮精装书，而是一张能被新定理反向调用、向前追溯的网络。📚 主要信源
- FormaTheoria 团队，《7个月超15数学家6年工作量，AI写下百万行代码挑战核验超大数学证明工程》，腾讯新闻（返朴转载），2026-08-31，https://news.qq.com/rain/a/20260831A04WXM00
- FormaTheoria 项目论文 arXiv:2608.10894（项目 8 月快照）
- 项目代码仓库：https://github.com/Qiuzhen-CFSG/CFSG
- Stephen D. Smith，《Applying the Classification of Finite Simple Groups: A User's Guide》，美国数学会，2018（231 页 / 10 章 / 14 个应用专题）
- Chris Hsu，《How One Programming Language Rewrote Mathematics and Why Software Is Next》，IBTimes / Web Pulse，2026
- 中国科学院外籍院士丘成桐推动该项目相关报道
Topic tag**：
#AIforMath #Lean #CFSG #清华