Lean 内核被 AI 攻破之后：v4.35.0 带上五个证明内核，两个完成形式化验证

开源AI安全形式化验证编程语言

AI 生成的数学证明能不能信，取决于最后把关的验证器本身有多可靠。10 月 15 日发布的 Lean v4.35.0 给这个问题一个工程答案：这个定理证明器现在自带五个证明内核，其中两个是经过形式化验证的，一条命令就能让它们交叉复检同一批证明。

leanprover/con-leche：带一致性证明的外部 Lean 检查器

Lean 是当下 AI 数学生态的验证底座。OpenAI 用它验证 Navier-Stokes 千禧年难题的 166 页证明，Claude 用它在 11 天里写完费马大定理 1300 万行的形式化，Anthropic 的 FLT 项目体量超过 1300 万行代码。这些证明是否成立，最终由 Lean 内核裁决。过去三个月里，这个裁决者自己被反复攻破过。

内核先被攻破，再被补强

7 月 25 日，密码学家 Ramana Kumar 发布了一个没有 sorry 占位符的 Collatz 猜想"反证"。Collatz 猜想是悬置近百年的数论难题，一个真正的反证足以震动数学界，但这个证明是假的：它利用了 Lean 内核处理嵌套归纳类型时的一个实现漏洞。当归纳类型 T 的参数是"幻影参数"（不出现在构造器字段里）时，内核生成的辅助类型会把这些参数丢掉，藏在那个位置上的类型错误就此逃过检查。攻击者借道元编程把恶意声明直接递给内核，就能让内核接受 False 的证明，等于让整个系统接受任何命题。

7 月 28 日，Kiran Gopinathan 把它缩减成一个小型 False 证明并提交 issue #14576，Lean FRO 一小时后推送修复。反常的地方在于：这个漏洞利用同样骗过了 nanoda，一个用 Rust 独立实现的第三方内核。事后复盘发现这是两个互不相干的 bug 叠加，官方内核漏检了嵌套归纳的位置，nanoda 则没有校验投影节点里的类型名。假证明恰好构造在官方内核不看的位置、而那个位置旧版 nanoda 恰好放行。独立实现互查的防线没有失效，但它要求每条实现链路都保持最新。

真正的压力测试在 8 月。OpenAI 的 Daniel Selsam 把 OpenAI 内部模型接入 Lean FRO，从 7 月 30 日找到 8 月 20 日，模型报告找不到新问题为止。这一轮挖出的漏洞比第一轮更深：一个是运行时引用计数溢出，溢出后内存被改写，内核照样接受 False；另一个更出乎意料，Lean 官方 Linux 发行版为了兼容旧 libc 一直在链 GMP 6.1.2，而这个大数运算库的已知缺陷被模型做成了假证明。8 月 21 日发布的 v4.33.1 修掉了全部问题，GitHub 上从此多了 soundness 和 runtime-soundness 两个标签，分别标记逻辑漏洞和运行时漏洞。

整个攻防过程有一条清晰的主线：官方内核是 C++ 手写实现，实现永远可能有 bug。归纳类型的处理、isProp 判定、def-eq 缓存的顺序依赖，每处都是新的攻击面。只要内核是"信出来的"，这类漏洞就会源源不断。

con-leche：用 Lean 写的内核，证明自己不收假货

v4.35.0 的回答是釜底抽薪。新内核 con-leche（CONSistent LEan CHEcker）用 Lean 语言写成，并且用 Lean 证明了自己的一致性：凡是它接受的证明，在集合论模型里都存在解释，因此不可能接受 False。这个性质由 no_False_declaration 定理陈述——任何包含 theorem : False := ... 声明的导出文件都会被它拒绝。证明本身由官方内核检查。

实现和证明都出自 Claude（Fable 与 Opus），在 Lean FRO 的 Joachim Breitner 监督下完成，仓库的 README 特意注明是人为写作、仓库里其余部分几乎都是 AI 产物。con-leche 没有复用官方内核的 Lean.Expr 类型，避免了底层未经证明的 C++ 例程；它用局部无名表示加 de Bruijn 层级自建项表示，只接受三个标准公理，见到其他公理直接拒绝。

让自研内核真正可用的关键是性能。形式化验证的实现对性能常有数倍损耗，con-leche 没有这个问题：官方性能测试里，检查完整 Mathlib（250 万行、69 万条声明、导出文件约 6 GB）时，con-leche 执行的指令数是官方内核的 0.69 倍，八个线程约 100 秒完成。验证过的实现反而比原实现少做工作，因为它采用统一的归纳类型处理策略，不做官方内核那套嵌套转互递归的归约。

con-ron 与多内核复检

con-leche 还剩一个信任缺口：它的证明不覆盖编译器和运行时，如果编译器生成机器码时引入错误，验证过的源代码也可能编译出错的程序。Lean FRO 的对策是让 AI 把 con-leche 翻译成 Rust，再用 Aeneas（一个把 Rust 程序翻译成 Lean 函数做验证的工具）证明 Rust 版本与原版算法精化等价，这个内核叫 con-ron。同一个证明分别交给 con-leche 和 con-ron 检查，两套编译器、两套运行时同时出错才算失守。

配套的复检入口是新的 lake check 命令。它把项目导出后交给 leanchecker（官方内核的精简版）在沙箱里复检，加 --paranoid 参数则依次跑 nanoda、lean4lean、con-leche、con-ron 四个外部内核，外加一个用加固内存分配器构建的官方内核变体，内存损坏会变成显式报错而不是静默的错误答案。发布博客给出的建议只有一句：在自己的项目上跑一次 lake check --paranoid，如果有内核对某个证明意见不合，Lean FRO 想知道。

v4.35.0 里 lean4lean 的验证尚未完成，官方预期几个月内收尾。它的价值在另一侧：lean4lean 的实现紧跟官方 C++ 内核，验证它等于对官方实现逐行审计。内核重构计划（issue #14977）由 Arthur Adjedj 推进，每个改动都要同步打进 con-leche 的证明，保证重构不引入新洞。

对 AI 数学生态意味着什么

Lean 内核的权威建立在它比前端简单得多、可以被人脑完整核查这个前提上。核 False 接受的 bug 动摇的是这个前提，而 verified kernel 把它重新钉回去：con-leche 的一致性证明覆盖了内核实现这一整类错误，剩下需要人工信任的只有集合论的一致性、Lean 编译器和 Rust 编译器，而最后一项已被 con-ron 对冲。

规模是下一道坎。Mathlib 250 万行，Anthropic 的 FLT 超过 1300 万行，General Courtade–Kumar 定理仓库已经超过 5000 万行，社区里在讨论 10 亿行量级的数学库提案。导出文件随体量线性膨胀，官方博客明确承认现有的外部内核方案撑不住这个规模，二进制导出格式和增量检查已经排上工作清单。

对工具链的使用者，这套机制不要求改变工作方式，lake build 照旧，代价只是需要强保证时多跑一条 lake check --paranoid。差别在于信任的来源：以前是"官方内核没出过事"，现在是"五个独立实现看完都点头，其中两个带机器检查的一致性证明"。

参考来源：