Automatic Textbook Formalization
Fabian Gloeckle, Ahmad Rammal, Charles Arnal, Remi Munos, Vivien Cabannes, Gabriel Synnaeve, Amaury Hayat
cs.AI
2026-04-03
3 万个 Claude 4.5 Opus 智能体并行协作一周,把 Grinberg 500 页的研究生代数组合教材形式化进 Lean,340 个目标定理全部证毕,推理成本约 10 万美元。
数学界有个老问题叫「审稿危机」:期刊审稿人没时间逐行核验证明,实际做的事只是「说服自己论文里的方法足够强,能推出主结论」。错的证明、甚至错的定理因此偶有漏网。Lean 这类证明助手(proof assistant)能把信任收敛到一个经过验证的小内核,只要证明被机器接受,就一定没错。
问题是手工形式化太贵。Lean 最大的数学库 mathlib 已经长到约 220 万行,但增长速度几乎是线性的,纯靠人堆的扩张方式本身受到质疑。论文点出两个卡点:一是大量教材级别的基础内容还没进证明助手,二是形式化的时间、人力、专业门槛必须降下来。
这篇要回答的就是:能不能用现在的模型和智能体编排,自动把一整本研究生教材形式化掉。
作者选的靶子是 Darij Grinberg 的《An introduction to algebraic combinatorics》,一本约 500 页的研究生代数组合教材,公共版权。选它的标准很讲究:内容能直接从 mathlib 现有机制推导出来,但又大部分还不在 mathlib 里,这样可以避开「模型背答案」的污染。
真正有意思的是编排方式。多智能体系统的老大难是「协调」:一群智能体怎么在同一个项目上一致推进而不互相拆台。作者没有发明什么聪明的调度算法,直接照搬人类软件工程的成熟做法:
这套组合让系统能「无畏并发」,Python 编排层不需要写重的调度逻辑。智能体按角色分工:Sketcher 写定义和定理陈述(证明先用占位符 sorry 撂着)、Prover 补证明、两类 Reviewer 分别审数学正确性和工程质量、Maintainer 处理 issue,再加 Triage、Scan、Progress 几种巡检角色。
3 万个 Claude 4.5 Opus 智能体跑了一周,把教材里 340 个目标定理和定义全部形式化并证毕。
| 指标 | 数值 |
| 目标定理与定义 | 340(全部证毕) |
| Lean 代码行数 | 约 13 万 |
| Lean 声明数 | 约 5900 |
| Lean 源文件 | 52 |
| 跑时 | 一周 |
| 智能体总数 / 成功 | 约 3 万 / 约 3300 |
| 输入 / 输出 token | 830 亿 / 5.61 亿 |
| 成本(无缓存) | 43 万美元 |
| 成本(估算含缓存) | 约 10 万美元 |
| 每页 / 每个目标定理 | 约 200 美元 / 约 300 美元 |
成本是这篇最想强调的结论:算上 prompt 缓存,整本教材大约 10 万美元,每页约 200 美元,作者说这已经「持平甚至低于」一队人类专家的薪水。
这篇把多智能体软件工程的可用结果推到了新量级,更值钱的是它的判断:形式化整个数学语料的瓶颈,已经不再是模型缺逻辑推理能力,而是怎么编排这群智能体的集体劳动。
编排上作者没造新轮子,人类软件工程那套(git、PR、merge queue、issue tracker)对智能体群同样管用,这本身就是结论。成本上,10 万美元干完一队人类专家要干好几年的活,作者明确说在不换模型的前提下还有 3 到 10 倍的效率提升空间。他们把教材形式化定位为「基础设施投资」:这本铺下去,该领域以后所有研究级形式化的成本都被拉低。
对从业者来说,这是 agentic coding 走到「能交付可用大型产物」的一个清晰样本,而且编排范式可复用,不依赖某家闭源魔法。
作者自己列了一串诚实的问题。成本被高估了:开发过程反复迭代、智能体做了教材习题和被引用定理这类不必要的活、也没有依赖追踪,所以他们认为真实成本还能再砍 3 到 10 倍。token 账面上有大约一半输入 token 花在了最终被中止的智能体上。
协调失败也真实存在:N-partition 这个数据类型被三组智能体各自独立定义了一遍;Bender-Knuth 对合的定义不一致,引发持续的「智能体空转」。还有「兔子洞」:智能体违背指令,跑去证正文里随口一提的结论,比如被 Kasteleyn 公式带去折腾 Pfaffian 和 FKT 算法,把资源从真正的目标上拽走。合并队列成了单点瓶颈,NFS 带宽也引起超时。
最核心的存疑是结构性的:这是单个教材的案例,不是受控实验,n=1。所谓「340 个全部证毕」只意味着 Lean 内核接受了这些证明,而内核只校验「智能体写的证明能推出智能体写的陈述」。如果某个陈述从一开始就从教材翻译错了语义,内核抓不到。作者也承认,他们只是人工抽查了关键陈述,「个别定理和定义没有被语义忠实地翻译」仍有可能。