事件与背景

这件事要看两条时间线，它们在 10 月交汇。

第一条是「内核被打穿」。7 月 25 日，Ramana Kumar 发布了一个不含 sorry 的 Collatz 猜想「反证」——由 AI 辅助生成。它不是真证明，而是利用了 Lean 内核在处理嵌套归纳类型时的一个漏洞（issue #14576）：当参数是 phantom（未出现在构造子字段中）时，它们会从生成的辅助类型里消失，从而逃过类型检查。7 月 28 日 Kiran Gopinathan 把它压缩成一个小型的 False 证明并提交 issue，官方一小时内推送修复。更值得警惕的是，独立检查器 nanoda 当时也没拦住：它自己有另一个互不相关的 bug（投影节点未校验类型名），两个 bug 叠加，才让那份「证明」同时骗过两个实现。

第二条是「主动狩猎」。7 月 30 日到 8 月 20 日，OpenAI 的 Daniel Selsam 用内部模型对 Lean 内核和运行时做了一轮 bug hunt，又找出多处可构造 False 证明的问题：对象引用计数溢出导致内存损坏、Linux 发行版链接的 GMP 6.1.2 存在已知漏洞、is_prop 实现未要求 sort、is_def_eq 缓存顺序相关等。8 月 21 日发布的 v4.33.1 一次性修完，GitHub 上新增了 soundness 与 runtime-soundness 两个标签。

然后是 10 月的回应。10 月 12 日发布的 Lean v4.35.0 把 lake check 和 lake comparator 做进了 Lake：构建、导出，再把结果送进 bubblewrap 沙箱重放给内核，任何非标准公理都会让命令失败。10 月 15 日 de Moura 的博客补上了最关键的一块——工具链现在自带四个独立内核：nanoda、lean4lean、con-leche、con-ron，外加一个用硬化内存分配器编译的 leanchecker-paranoid；lake check --paranoid 要求所有实现都接受，才算通过。

其中 con-leche 是第一个用 Lean 编写、并在 Lean 里证明了一致性的 Lean 内核：它接受的环境都能在集合论里找到模型，因此从根上排除了「内核实现写错」这一类 bug。README 写得很直白——实现和一致性证明都由 Claude（Fable 与 Opus）完成，Joachim Breitner 在 Lean FRO 重度监督；「这个 README 大概是仓库里唯一由人类写的东西」。性能也没有牺牲：完整 Mathlib 导出约 100 秒（8 线程），指令数为官方内核的 0.69 倍。con-ron 则是把 con-leche 用 AI 翻成 Rust，再用 Aeneas 证明 Rust 版本细化（refine）了原算法——两套编译器与运行时同时出同一个 bug 的概率极低。

来源（均已用 curl 验证返回 200）：

• Lean Now Ships with Verified Kernels — Leonardo de Moura（2026-10-15）
• Lean v4.35.0 Release Notes（2026-10-12）
• Postmortem for Kernel Soundness Bug #14576（2026-08-01）
• Postmortem for the Kernel Soundness Bug Hunt（2026-08-24）
• con-leche 仓库（含一致性与性能说明）、con-ron 仓库

为什么现在重要

1. 「验证通过」的信任根，正好落在 AI 的攻击面上。 过去证明助手威胁模型里的人是「可能写错证明的数学家」，现在是「会主动构造能骗过检查器的证明的模型」——7 月那份 Collatz 反证就是被模型找出来的路径。影响：形式化验证的产物不再是一张免审证书，而是一条需要做威胁建模的供应链。

2. 信任模型从「单一实现正确」改成「多个实现的交集」。 四个内核加硬化分配器版本，全部接受才算过。这是安全工程里 N-version programming 的老办法，但第一次被做进主流证明助手的默认工具链，而不是论文里的原型。影响：以后「Lean 验证过」这句话必须补上「用哪个内核、哪些内核一致」。

3. AI 同时当攻击者和修补者，闭环周期被压到周级。 7 月模型找到漏洞，8 月模型参与狩猎，10 月模型写出并证明了一个从设计上排除该类 bug 的内核。影响：安全团队「红队发现—修复—再验证」的节奏会从季度变成周，人的角色上移到定义规范、审查证明假设与监督过程。

4. 成本终于低到可以进 CI。 以前跑外部内核要自己装 nanoda、lean4lean、comparator 并手工导出；现在是随工具链分发的一条命令，Mathlib 量级 100 秒。影响：这不是发布会 Demo，中小项目今天就能挂进流水线。

5. 但规模化问题被明确承认还没解。 外部内核要全量导出再重放：Mathlib 2.5M 行、Tau Ceti 已超 3M 行、Anthropic 的 FLT 超过 13M 行、General Courtade–Kumar 定理仓库超过 50M 行，社区已在提 1B+ 行的数学库方案。de Moura 直言当前的外部内核方案撑不到那个体量，需要二进制导出格式和增量检查。影响：现在能用，但只对中小规模开发成立。

工程师/产品人今天能做什么

1. 把 lake check 加进 CI，发布产物再跑一遍 lake check --paranoid。 默认档只跑官方内核；--paranoid 才跑全部四个外部内核加硬化版本。分别记录每个内核的结果，不要只看命令的 exit code——「哪个内核拒绝了」才是有用的信号。
2. 把非标准公理当成构建错误。 lake check 会在使用标准三公理（propext、Quot.sound、Classical.choice）之外的公理时失败。把 sorryAx、自建 axiom 从「警告」提升为「阻断合并」，这一步比换内核更能防住大多数假证明。
3. 固定并记录检查器版本。 检查器自己也会修 bug——nanoda 就曾漏掉投影节点的类型名校验。把 Lean 版本与各内核的 commit 写进产物元数据；用旧版检查器复核新证明，等于假设历史漏洞不存在。
4. 对外表述改口径。 如果产品把「已形式化验证」当卖点或合规证据，改成「Lean 4.35.0，官方内核 + nanoda + con-leche 一致通过，公理白名单为 X」。采购第三方形式化成果时，同样要求对方给出这份清单，而不只是一句「已验证」。
5. 用 lake comparator 校验「证明的定理 == 你声称的定理」。 给它一个 challenge module 和一个 solution module，它会逐条确认定理陈述一致、只用了白名单公理、内核接受。对外部交付的形式化模块，这比读代码可靠得多。

待观察

• lean4lean 的验证预计「未来几个月」完成，届时官方发行版将有三个已验证内核。另外要注意：con-leche 的一致性证明本身建立在所用集合论模型一致的前提上，这个假设不在证明覆盖范围内——它是「相对一致性」，不是绝对保证。
• 增量检查与二进制导出尚无时间表。1B+ 行级数学库的提案一旦落地，当前「全量导出再重放」的路线会先撞墙，这可能决定下一代工具链的形态。
• 归因仍未证实：7 月那次时间重合，Ramana 认为纯属巧合，也无法排除模型见过 nanoda 的报告；Joachim 的假设是「强模型让这类 bug 更容易被发现」。目前没有公开证据表明有生产系统因这类内核 bug 被实际攻破。