AI 构造假证明破解 Lean 4？剥开内核 #14576 漏洞与形式化验证的信任真相

2026 年 7 月下旬，形式化验证社区发生了一件令人震动的事件：研究员 Ramana Kumar 在 AI 模型的辅助下，提交了一份针对著名数学难题“考拉兹猜想”（Collatz Conjecture）的伪反例证明。

令人警惕的是，这份推翻考拉兹猜想的证明中没有包含任何 sorry 占位符，却被世界顶级证明助手 Lean 4 的内核顺利接受并编译通过。

一时间，社交媒体与 Zulip 讨论组大受震撼：难道数学逻辑的守门员真的被 AI 攻破了吗？

紧接着在 7 月 28 日，研究员 Kiran Gopinathan 将该代码精简为一个几行即可推出 False（逻辑矛盾）的最小复现样例，并向 Lean 官方仓库提交了致命的 Issue #14576。Lean 缔造者 Leonardo de Moura 与团队在 1 小时内火速推修补 PR #14577 并完成合并。

这不仅是一次高效率的漏洞修补，更是一场关于“形式化验证在 AI 时代究竟信任什么”的经典案例。

一、幻影参数逃逸：漏洞到底发生在内核何处？

要理解这次事故，首先要分清数学理论（Meta-theory）与软件实现（Implementation）的界限。

Lean 的底层逻辑元理论依然健全。这次漏洞完全是一个典型的软件编码实现缺陷，发生在内核处理**嵌套归纳类型（Nested Inductive Types）**的消除器（Eliminator）逻辑中。

在代数数据类型中，归纳类型可以带有参数（Parameters）。当某个参数存在于类型声明中，却未在任何构造函数（Constructors）的实际字段中显式引用时，它被称为“幻影参数”（Phantom Parameter）。

Lean 内核在生成辅助消除类型时，原本应该对这些参数进行严格的类型检查。然而在嵌套归纳类型的消除路径上，实现代码出现了一个疏漏：幻影参数在消解过程中被悄然丢弃，从而逃脱了内核的类型检查（Type Checking）。

攻击者正是利用这一漏洞，构造了一个带有非法类型参数的声明直接发给内核，使得内核在推导时错把一个非法项识别为合法表达式，进而推出了空类型（Empty Type）的元素，即证明了 False。

二、架构隔离：为什么“关闭元编程”是错误的药方？

漏洞曝光后，社区有一种声音认为：“攻击者是通过 Lean 的元编程（Metaprogramming）API 直接向内核注入原始声明才成功触发漏洞的，因此应当限制或取消元编程。”

Leo de Moura 在复盘报告中明确驳斥了这种看法。这种观点代表了对证明助手架构设计的深刻误解。

在现代证明助手（如 Lean、Coq）的经典架构中，系统被严格划分为两部分：前端 Elaborator（负责语法解析、类型推导和宏展开）与底层 Kernel（只负责最终语法树的类型校验）。

| Trusted Kernel (Small) |` -->

Elaborator 在设计上就被假定为“不可信”（Untrusted）的。

内核的安全健全性（Soundness）绝不能建立在“前端拒绝生成坏代码”的前提上。任何恶意攻击者完全可以绕过 Elaborator，通过修改 .olean 字节码文件甚至注入进程内存来提交畸形声明。

内核必须像一个独立的沙箱进程一样，依靠自身的独立校验逻辑拒绝任何不合法的声明。这种将推导逻辑与检验逻辑彻底隔离的“Small Trusted Kernel”（小信任核 / de Bruijn 原则），正是形式化证明区别于普通软件测试的核心价值所在。

正如我们在分析软件质量与验证瓶颈时所指出的，重写的瓶颈从来不是写代码，而是如何建立不可动摇的验证边界。

三、双重漏洞交叠：第三方 Rust 内核为何最初没拦住？

证明助手体系的另一重终极防御，是独立第三方内核（External Independent Checkers）。即便官方 C++ 内核出了 Bug，只要用不同语言实现的第三方内核拒绝接受，攻击依然无法通过。

然而在这次事件中，Ramana 的伪证明居然也通过了由 Chris Bailey 用 Rust 开发的独立检查器 nanoda。

难道第三方检查器也失效了吗？答案令人吃惊：这是两处完全无关的 Bug 在同一时间窗内的巧合交叠。

官方 Lean 内核漏掉了嵌套归纳类型的参数消除检查；而 Rust 版的 nanoda 实际上写了那段检查，却在另一个无关的地方（投影节点的类型名校验）存在一个失误。而 AI 辅助生成的证明表达式，碰巧踩在了两个内核各自缺陷的交叉盲区里。

事实上，nanoda 的该缺陷在一周前就已被研究员 Jeremy Chen 发现并修复。如果使用最新版的 nanoda，这份伪证明在第一时间就会被 Rust 检查器拒之门外。

这也印证了系统安全中的一个基本常识：多核交叉验证（Multi-kernel Checking）依然极其有效，但前提是必须保持所有独立检查器的实时更新与持续跟踪。正如 Palantir 在工程实践中所强调的，从 Demo 到生产：为什么 Palantir 认为大模型需要“单元测试”？，真正的系统可靠性来自于多重验证回路的严密闭环。

四、AI 的双刃剑：从“漏洞制造者”到“内核审计官”

在这场攻防演练中，AI 展现出了双重角色。

一方面，强力的 LLM 具备了在复杂类型系统中探索极端边缘分支的能力，能够辅助研究员拼凑出人类难以察觉的漏洞利用链；

另一方面，Lean FRO 团队也在与 OpenAI 的 Daniel Selsam 合作，利用针对网络安全专门微调的 AI 智能体，对 Lean 内核代码进行深度的自动化模糊测试与隐患挖掘。

在漏洞 #14576 修复后，专门的安全 AI 智能体又协助团队在 Lean 内核中发现了多处潜在的编程疏漏（PR #14607 至 #14616），目前已全部完成修补与不变量硬化。

这标志着形式化验证生态正在迈入一个新的阶段：AI 既是高强度的压力测试者，也是内核代码硬化的自动化审计官。

总结：信任从不建立在“绝无漏洞”的幻觉上

Lean 4 内核漏洞 #14576 的复盘，给所有关注 AI 与软件验证的人上了一课。

形式化验证的真正威力，从来不是保证底层实现代码由神圣不可侵犯的上帝编写、绝无任何软件 Bug；

它的真正价值在于，它将人类对“数学真实”的信任，从几百万行庞杂的前端编译器、宏系统和 AI 大模型中剥离出来，重新收敛到了一个仅有几千行、可随时被开源审计、可被 Rust 等独立第三方内核交叉印证的极小信任核中。

只要这个极小内核保持独立隔离与持续硬化，任何通过漏洞滑过的“伪证明”都会在几小时内被彻底揭露与消灭。

在 AI 生成代码呈指数增长的今天，这种将信任界限收敛至极小核的工程智慧，或许正是我们在不确定性世界中守护确切性的唯一基石。

如果在你的工程实践中，也需要为关键系统构建不受信任前台干扰的信任核，你会选择怎样划定边界？欢迎在评论区分享你的看法。