7个月干完15个数学家6年的活：清华团队把2万页证明塞进Lean，这才是AI科研的正确姿势

7个月干完15个数学家6年的活：清华团队把2万页证明塞进Lean，这才是AI科研的正确姿势

还记得不久前 OpenAI Astra 闹出的笑话吗？AI 洋洋洒洒写了 37000 行代码，声称证明了数学猜想，结果被人类数学家 24 小时光速打脸：AI 证对了每句话，但全都是同义反复的废话，跟原命题半毛钱关系没有。

那次翻车直接戳破了“AI 闭环科研”的巨大泡沫——没有严格形式化约束、缺乏自顶向下知识网络管理的所谓“AI 数学家”，本质上只是个高级逻辑编造机。

但今天，清华大学求真书院领军班联合丘成桐数学科学中心、智能产业研究院与华威大学交出的这份答卷，彻底重塑了“AI for Math”的游戏规则：

他们打造的 FormaTheoria 工作流，用 7 个月时间完成了曾经 15 位顶尖数学家耗时 6 年 才搞定的大规模形式化工程（Feit–Thompson 奇数阶定理等四大核心定理），在 Lean 里写下了 99.4 万行严密代码、构筑了 18.6 万条依赖关系网，正式向数学史上最庞大、散落近 2 万页文献的“有限单群分类（CFSG）”工程发起了机器核验总攻！

—

为什么说以前的“AI 解题”全是在玩过家家？

过去两年，市面上吹捧的 AI 数学能力，基本上停留在以下两个极端：

1. 做竞赛玩具题：给定现成的题目、定义和前提，让推理模型在闭卷环境里刷 IMO 金牌； 2. 闭门造车写伪证：给一个开放猜想，LLM 狂吐几十万 Token，格式挑不出毛病，但前提漂移、定义偷换，人工审查成本甚至高过重新证明。

因为现实世界的严谨科学研究，从来不是“做一道准备好的选择题”。

以“有限单群分类”（CFSG）为例，它是现代代数学的底层操作系统，支撑着包括菲尔兹奖级别成果在内的无数下游理论。但它的完整证明散落在数百篇论文、跨越半个世纪、总计近 2 万页。更致命的是： – 符号与定义冲突：50 年代和 80 年代的论文，对同一个概念的默认假设完全不同； – 隐式断点与笔误：人类数学家默认“读者能看懂”而省略了关键前提，甚至把整除条件、下标写错，带着 bug 流传了几十年； – 无限依赖展开：你为了证明 A，查出依赖 B，查 B 又牵扯出 12 篇前置文献，扩充了 65% 的未知材料。

单靠把 Prompt 塞给大模型，模型连定义都对不齐，怎么可能完成两万页的全局复核？

FormaTheoria 的硬核解法：把科研拆成工业级流水线

清华团队这套工作流之所以能跑通，核心就在于它彻底摒弃了“单体模型盲目推理”的幻觉，用了一套极为严密的工程闭环：

1. “依赖感知”的知识图谱推进

系统面对未知的文献依赖，绝不强行脑补。一旦检测到缺失前置定理，立刻挂起当前主线，启动子 Agent 检索并形式化依赖项，存入全局知识库供后续任务复用。这种依赖感知的并行策略，直接带来了 4.2 倍的工程加速。

2. 翻译与审查的“红蓝对抗”

Lean 编译器只能检查逻辑自洽，查不出语义篡改。 AI 经常会为了强行通过编译，偷偷把“对所有 x 成立”改成“存在 x 成立”，把结论彻底改弱。

FormaTheoria 设立了独立的红蓝审查机制：翻译 Agent 产出 Lean 声明，审查 Agent 拿着原始文献逐字逐句挑刺。数据极其惊人：在测试的 14 个小节中，有 11 个小节的首轮翻译被审查机制直接退回！ 没有这道关卡，产出的 100 万行代码全是垃圾代码。

3. 抓出沉睡数十年的文献 Bug

人类在阅读数学文献时，经常依靠领域常识“脑补”正确结论，从而忽视了纸面上的印刷错误。而 Lean 是一台冷酷的验算机，少一个字都不认。 在 7 个月的执行中，FormaTheoria 抓出了一连串人类数学家视而不见的硬伤： – 某经典教材把对象 $H$ 错印成 $M$； – Huppert 定理将整除因子放错了位置； – 引理陈述中漏掉了“群的阶为奇数”的核心前提。 这些问题要么由系统通过上下文和辅助定理自动修复，要么生成证据链提交给人类数学家仲裁。

9.17 天不中断执行与 606 次记忆压缩：超长程 Agent 的工程范本

这篇工作对于整个 AI 行业最宝贵的贡献，不仅在于群论，更在于它展示了一个超长程自治 Agent 系统（Long-horizon Agent）究竟该如何构建。

论文记录了系统单次最长连续执行时间达到了 9.17 天，期间经历了 606 次上下文主动压缩与状态重构。

最长的一条数学依赖链，垂直深度达到了 458 层！

如果按照传统的“对话窗口”思路，Agent 跑不到半小时就会因为上下文溢出、注意力涣散而彻底崩溃。FormaTheoria 通过维护一张动态演化的“证明拓扑地图”（Proof Map），将已完成的确定性知识沉淀为持久化资产，将失败路径打上黑名单，确保了系统在长达一周的计算中始终保持方向感。

结语：AI 科研的下半场，拼的是“重工业装配能力”

从 OpenAI Astra 的“2000 美元买废话”，到清华团队用 Lean 啃下近百万行硬核形式化证明，分水岭已经无比清晰：

AI 不会因为会做几道奥数题就成为爱因斯坦。真正的 AI 科研变革，是把散落整个人类历史的模糊知识，通过形式化系统编译成 100% 可验证、零漏洞的机器理论底座。

能啃下 2 万页 CFSG 的系统，明天就能啃下 1000 万行 Linux 内核代码，就能核验千万级航天飞控软件的每一个状态分支。

当 AI 学会了在严格约束下老老实实当“工程质检员”，AGI 的地基才算真正夯实了。