一个研究了两辈子证明的人，提醒你别迷信检查器
10 月 9 日，数学家 Thomas Hales 在陶哲轩博客发了篇客座文章。此人的分量摆在这儿：开普勒猜想——三维球堆积，悬了将近四百年——他的证明两百多页，审稿人承认看不完；他随后花了约二十个人工年，把整个证明形式化进 Lean。这样一个人说「机器检查的证明，也别全信」，行业得听。
文章的背景是 AI 自动形式化今年真的落地了：用 AI 把数学论文翻译成 Lean 这类可机器检查的证明，从演示变成了日常。Anthropic 9 月初宣布用 11 天把费马大定理写成 1300 万行 Lean；OpenAI 9 月 8 日公布了带 Lean 证明的 Navier-Stokes 结果；mathlib 库已经有约 30 万条定理、250 万行代码、七百多位贡献者。Hales 的判断是：这件事今年越过了「实用」线——而他紧接着讲的，是这个夏天 Lean 内核接连出事的故事。
soundness 之夏：检查器被绊住的六周
Hales 管七八月叫「Summer of Soundness Bugs」。最扎眼的一起：7 月有仓库贴出「Lean 验证的 Collatz 猜想伪证」——不是行为艺术，Lean 内核真的接受了它；独立的检查器 nanoda 也接受了，通过的是另一个互不相干的 bug。研究者 @kiranandcode 用三天把问题追回内核本身，正式报告提交后一小时，补丁就落了地。同一个 bug 还产出过一条「开普勒猜想」的短伪证——正是 Hales 钻研了二十年的那个定理，他得知时的荒诞感可想而知。
账要记全：8 月 21 日的 Lean v4.33.1 修了 5 个内核加 2 个运行时 soundness 缺陷；8 月 24 日 de Moura 的事后分析里写着，OpenAI 一位研究者用网络安全专用的 AI 协助 Lean FRO 又找出若干缺陷，直到内部模型报告「找不到更多了」。Hales 特别强调这是好消息——找到漏洞的是前沿模型加安全研究员，不是攻击者。另一条冷记录同样刺眼：用公开模型的小组，一个 bug 都没报出来。工程响应速度也值得肯定：一周内修复、mathlib 用修好的内核重新验证过。
但修完 bug，地基的问题还在
Hales 真正在意的是结构。Lean 的内核本身没有经过形式化验证；它的类型理论至今没有完整的公开相对一致性证明；Carneiro 2019 年那篇奠基性的类型理论论文里有错；「每个项的类型是否单一」这个问题还没被证出来；定义相等在一般情形下不可判定。理论上有个 --trust=0 模式号称能抓住任何畸形证明，可现实是：AI 探测内核的速度，已经快过人审内核的速度。
他给的方向是冗余与独立：多个互不抄代码的内核交叉验证（Navier-Stokes 的形式化已经过了 12 个以上检查器确认，Lean 内核竞技场里躺着约 25 个内核），以及 Breitner 的 Con-Leche——一个自带形式一致性证明、已经复核过 mathlib 的检查器（代价是假设一套带不可达基数的 ZF 编码）。他还刻意提了 Thompson 那篇《信任信任》：你没法用验证器验证验证器，到某一步必须有人去审那层地基。
为什么智能体行业该读这篇
把主角换掉，这个故事每天都在Agent 圈上演：AI 产出、机器验证、验证通过即采信—— verified code、verified AI output，底层是同一个信任假设。这篇博文给出的增量认知有三层。其一，验证链上每一环都是攻击面，而 AI 同时是作者和审计者，两条时间线并行跑。第二，Hales 的规则朴素得该抄进每个流水线：内核检查通过之前不要信任何证明；同时，让人确认「证的还是原来那个命题吗」——陈述保真度是验证管不了的那道缝，719 篇 AI 数学手稿那场「形式化比例」之争（约四成过 Lean）争的正是这个。第三，本站 1194 写过多智能体数学发现系统、216 写过 Lean 系模型——那时叙事是「证明助手变强了」；这篇把叙事翻了过来：助手变强之后，该审计助手自己了。目前官方及行业暂未披露更多细节，后续将持续跟进迭代动态。