数学史上规模最大的证明工程——有限单群分类（CFSG）——第一次被 AI 系统性核验。由清华大学求真书院学生与丘成桐数学科学中心、智能产业研究院、华威大学研究者共同提出的 FormaTheoria 工作流，用 7 个月写下超过 99.4 万行 Lean 代码，完成了四个关键定理的形式化：Feit–Thompson 奇数阶定理、Glauberman Z* 定理、Brauer–Suzuki 定理、Bender–Suzuki 定理。
参照系很能说明问题：此前 15 位数学家花了 6 年，才在 Rocq（Coq）中完成 Feit–Thompson 定理的形式化。FormaTheoria 在 7 个月内干完了这个人工项目的全部内容，还继续向前延伸。
它不是「AI 解准备好的题」
多数 AI 数学系统拿到的是题目、定义和工具齐备的「现成题」，AI 只负责找证明。FormaTheoria 相反：它从零散的原始文献出发，先重建定理底下的数学基础——查文献、补依赖、对齐符号——再构造形式化证明，最后交给 Lean 证明助手逐步核验。
论文把难点拆成四道，每道都有工程解法：
- 不知道要读多少资料。一条引用牵出一篇论文，又引出更多前置工作。项目最初只有 3 个主要来源，过程中又发现 12 个；补上的材料占全部查阅页码的 65.6%。解法：发现缺前置定理就暂停当前证明，补完形式化再回来；已验证结果存进统一知识库，供后续证明反复调取。
- 文献之间接不上。不同作者对同一概念给出不同定义——数学上等价，写进 Lean 却不兼容。解法：搭显式转换桥，同时保护已核验的陈述，检查每处修复是否波及后续证明。
- 代码通过检查≠忠实原文。Lean 只查证明逻辑自洽、结论能否由前提推出，不查结论是否忠实于论文。AI 可能漏条件、混淆「所有」与「存在」、甚至悄悄改动结论。解法：设独立审查关卡——翻译组件先写 Lean 陈述，审查组件再对照原文逐项核对。论文分析的 14 个文献小节里，11 个首轮翻译被退回修改。
- 原文本身有错。两部资料对「类型 I 极大子群」定义不一致，系统用 Schur–Zassenhaus 定理证明两定义实际等价、搭起桥梁；Péterfalvi 一条引理漏了「群的阶为奇数」前提，系统自动补进陈述；Huppert 一条定理把因子写进错误的整除条件，系统找到反例后终止证明、交给数学家确认；连两部参考资料都保留了把对象 H 写成 M 的笔误。
超长程工程管理同样关键：一张持续更新的「证明地图」把大目标拆成引理、成功逐层汇回主定理、失败路线被记录避免重走死胡同；依赖感知的并行让共享前置结果只算一次（实测 4.2 倍加速）。最长一次智能体运行达 9.17 天，期间做了 606 次信息压缩整理，同时始终保留当前目标、已完成结果与待解问题。
最终数字：证明网络含 30,298 个数学声明、186,187 条依赖关系，最长依赖链 458 层；算上 Lean 标准库，扩大到 74,922 个声明、超过 144 万条依赖。
数学文献是一份没有编译器的 legacy 代码库
CFSG 约两万页、上百位作者、历时数十年，约定靠「圈内读者都懂」。从来没有编译器检查过它，错误藏在明处，因为熟练读者读着读着就自动纠正了。
形式化就是数学缺席多年的编译器：每个定义、每个条件、每步推理都必须写清楚。AI 干的不是「写证明」，而是把两万页系统的整张依赖图重建出来，并让它通过类型检查。核验只是可见的结果，真正的资产是底下那套可复查、可追踪的基础设施。
超出数学的意义
其一，AI 的能力边界在移动。从「解孤立题」走向「长期维护大型知识基础设施」：连续运行多天、压缩上下文、跨数十份文献追踪依赖、让跨周的任务线保持连贯。这是 Agent 能力的体现，任何拥有庞大互联知识体系的领域都适用。
其二，三层验证是可信 AI 的模板。一致性检查（Lean）+ 独立忠实审查（对照原文）+ 人工升级路径（证据不足时交给数学家）。AI 生成代码、合同、科学声明的场景都需要这个拆分：生成器可以流畅，验证者必须对抗，最终判断权在人。
其三，可验证的数学变成可复用资产。这张网络将像测试完备的代码库一样，成为未来定理研究的基础设施；接上搜索、解释、可视化工具后，研究者直接查询它，而不是重新推导。
其四，这是人机协作的现实版本。人决定研究什么问题、做关键判断，AI 承担大规模搜索与推导，形式系统保证每个被接受的步骤都能复查。当证明大到任何个人都无法通读，这种分工不是选择，而是唯一选项。
可操作的建议
- 做长任务 Agent：准备一张持久化的进度地图、记录失败路线、压缩记忆，共享依赖只算一次。
- AI 生成代码或声明：加一道独立忠实审查，对照你的真相源逐项核对。「通过校验」不等于「忠实原文」——这个项目里 14 个首轮翻译被退回了 11 个。
- 别把「机器核验」当「机器理解」：验证工具保证内部自洽，不保证对应意图。两层都要有，否则只有严谨、没有真实。
论文：arXiv:2608.10894 · 代码：github.com/Qiuzhen-CFSG/CFSG
