过去两个月，本站连续写过 OpenAI 数学的量产与撤稿、Lean 验证在其中的角色。但有一条主线一直没有展开：当 AI 生成的形式化证明以千万行计的时候，那个负责最终裁决的验证器本身，由谁来验证？ 10 月 9 日，陶哲轩的博客刊出一篇客座长文，作者 Thomas Hales——就是那位用计算机证明 Kepler 猜想的数学家——把这个问题摊开在了所有人面前。
一、一篇迟到的必读文献
Hales 这篇文章的标题是「数学家应该了解 Lean 定理证明器的什么：可靠性问题与 AI」。它出现在一个微妙的时点：过去一年自动形式化从理想变成了日常，而这篇文章在提醒大家，地基的验收标准还没人认真讨论过。
文章本身也有个耐人寻味的脚注：它最初用另一种文件格式写成，由 AI 转换成博客可用的格式，陶哲轩特意标注了这一点。一个讲「自动形式化可靠性」的文章用 AI 完成了排版转换——这个时代所有关于信任的讨论，都发生在 AI 已经深度介入工作流之后。
二、自动形式化的 2026：从二十年到十一天
Hales 先给了一组对照数字。他自己的 Kepler 猜想形式化花了约 20 个人年，产出 50 万行证明脚本。而 2026 年发生的事：
- 2025 年 9 月，Math Inc. 完成素数定理的「准自动形式化」——之所以算「准」，是因为 AI 卡住时仍需人类介入指路；
- 2026 年 1 月，Urban 发出预印本，两周内自动形式化了 13 万行拓扑学内容，覆盖 Munkres 教材的大部分；
- 2026 年 3 月，Math Inc. 在宣布完成 8 维球堆积形式化一周后，又完成 24 维球堆积的自动形式化，生成约 50 万行代码，剪枝后剩 20 万行；
- 2026 年 5 月，Meta 研究院的 ATLAS 项目自动形式化了 26 本数学教科书的大部分；
- 2026 年 9 月 4 日，Anthropic 宣布完成费马大定理的自动形式化，11 天生成 1300 万行 Lean；
- 9 月 8 日，OpenAI 宣布带外力的 Navier-Stokes 爆破定理证明时，附带了 Lean 形式化。
支撑这一切的 mathlib 库如今有近 30 万个定理、超过 10 万个定义、250 万行代码、700 多位贡献者。甚至有人发起了「数学自动形式化计划」（MAP），目标直白到吓人：把所有已知数学翻译成形式代码。作为参照，费马大定理那一项目的量级是 1300 万行——「下一个一万亿行代码」的提法已经出现在了正经讨论里。
三、Kernel：几千行 C++ 撑起的一切
Lean 的信任结构其实很清晰：证明脚本经过 elaboration（某种意义上的「数学编译」）之后，交给 kernel 做最终检查。kernel 是几千行 C++ 代码，是整个体系的最终裁判。
Hales 把责任边界划得很清楚：如果 mathlib 那 250 万行里混进了一个无条件为假的证明，那就是 kernel 的失职。反过来，kernel 通过的证明也不应被直接相信——还差一步「陈述保真」的人审：形式化的命题是不是你真正想证的定理？实数、偏导、测度这些定义是否与学界共识一致？这一步对 Navier-Stokes 来说，就是把 Lean 陈述对照千禧年大奖问题的官方表述核一遍，难度远低于检查证明本身，但不可或缺。
四、多事之夏：当 Collatz 被非法反证
然后是今年夏天的主角戏。soundness bug——允许 kernel 接受对 False 的证明的缺陷——是证明助手最灾难的 bug 类型，因为它意味着任何命题都能被「证明」。Hales 本人是这个领域的老猎人：2003 年他在 HOL Light 里发现过 soundness bug，那个内核只有几百行代码，此前七年无人发现。
Lean 4 在 2023 年 9 月发布前修掉两个；2025 年 5 月又报出一个溢出引发的。然后，2026 年春夏之交，业界现在称之为「soundness bugs 之夏」：七八月间多个 soundness bug 集中爆出，其中一个让 Lean 产出了 Collatz 猜想的非法反证——另一个让 Hales 本人在自己的老领域里收获了一份非法的 Kepler 猜想证明。
所有 bug 都被迅速修复，mathlib 已用修复后的 kernel 重新验证。但这件事的真正价值在于暴露了信任结构的细节。
五、三条防御路线与其天花板
Hales 讨论了三条堵漏路线，每一条都有清晰的天花板。
第一条：多内核交叉验证。 社区已经写了约 25 个 Lean 内核。Navier-Stokes 的形式化已被十几个证明检查器确认。但 Hales 用自己的遭遇给出了现成反例：Collatz 非法反证没有被 Nanoda 内核拦下，因为它自己带着另一个无关 bug 照单全收。不同内核可能共享同源缺陷，芯片有软错误、系统有漏洞、编译器会出错。理想状态是「洁净室」内核——实现者不看原版源码，避免把 bug 一起复制过去。
第二条：形式化验证 kernel 本身。 天花板是哥德尔第二不完备定理：足够强的系统无法证明自身一致。能做到的最好程度是相对一致性——假定基础系统一致，则 Lean 4 一致。这条路线历史悠久且仍在推进，但它注定是「相对的保证」。
第三条：陈述保真的人审。 前面说过，这是把指数难题压缩成可完成核对的一步，Lean 的 comparator 工具还能辅助检查未授权公理。
六、真正的转折点：AI 站在了验证这一边
这个夏天故事里最值得记住的角色分工，可能被大多数报道错过了。这些 bug 不是黑帽挖出来的，而是前沿模型在安全研究者手里挖出来的：
Collatz bug 的发现者 Ramana Kumar 是 CakeML——端到端经过形式化验证的 ML 编译器——的作者之一；多个其他 bug 由 OpenAI 的 Dan Selsam 协助 Lean FRO 找出，他带去的是一台专攻网络安全的内部 AI，逐个报出 kernel 的编程错误，直到 AI 自己报告「找不到更多问题」才结束合作。de Moura 随后发布了完整的事后分析。
把镜头拉远，这个结构意味深长：生成侧的 AI 十一天写出一千三百万行证明，验证侧的 AI 在同一个夏天给验证器做安全审计。 同一条技术曲线的两端，一边生产信任，一边检测伪信任。Hales 们担心的最坏情形——黑帽用 AI 找到 soundness bug 然后伪造重要定理——没有发生，但攻防双方都换了武器。
七、给工程师的三条提醒
这篇文章虽然是写给数学家的，对做 AI 系统的工程师同样有三条直白的提醒。
第一，「已验证」永远要追问验证器。 形式化验证不是信任的终点，而是信任的转移——从证明转移到 kernel。任何打着「数学上已证明」旗号的 AI 产物，都值得再问一句：哪个 kernel、什么版本、谁审计过陈述。
第二，保真审计不可外包。 证明正确但命题错误的形式化结果是真实存在的风险类别。无论自动形式化流水线跑得多顺，最后一步「确认它证的就是我们要证的」目前仍是人类职责，也是整条链路上性价比最高的一步人工介入。
第三，防御要赌多样性而非单点强度。 25 个内核、多种实现语言、不同硬件、洁净室设计——这套思路与安全工程里的 N 版本编程一脉相承。在 AI 同时武装攻防两端的年代，单点再强也不如异构冗余可靠。
Hales 在文章结尾没有渲染危机，反而把「bug 被找出来的夏天」定性为积极发展。这大概是这篇文章最冷静也最重要的判断：自动形式化的地基没有塌，但它第一次被认真地敲打了一遍——而敲打它的，恰好也是 AI。