AI 辅助的错误证明骗过 Lean：形式化验证的可信根也会出错
作者：林岚｜OC 开发者生态编辑
作者：林岚｜OC 开发者生态编辑
Lean 创始人 Leonardo de Moura 在事故复盘中确认，Lean 4 内核近期修复了一个健全性漏洞。一个借助 AI 生成的“考拉兹猜想反证”利用该漏洞，在没有 sorry 和额外公理的情况下通过了内核检查，但它并不是有效的数学证明。
一句话结论：AI 没有推翻考拉兹猜想，它只是意外找到了一条让证明检查器接受非法类型的实现路径；这反而提醒我们，形式化验证的可信度最终仍落在一个会写出 Bug 的软件内核上。
事情始于 7 月 25 日公开的一份短证明。三天后，研究者把问题缩减成一个可以直接证明 False 的最小案例，并提交 Lean Issue #14576。Lean 团队在报告后一小时推送修复，随后发布补丁版本。
漏洞发生在嵌套归纳类型的处理上。内核生成辅助类型时，会丢弃一组没有出现在构造器字段中的“幽灵参数”，导致这些参数绕过类型检查。攻击性元程序可以直接向内核提交构造后的声明，让一个结构投影作用在错误类型上，最后得到无公理的 False。
普通 Lean 语法前端会拦住这个错误，因此它不能靠日常证明代码直接触发，必须使用元编程接口构造声明。这是内核实现漏洞，不是 Lean 类型理论本身被证明不一致。问题严重之处在于，内核本来就是最后一道可信边界；一旦它接受声明，后续普通代码都可以引用这个错误定理。
更意外的是，旧版独立检查器 nanoda 也接受了原证明，但原因是另一处无关漏洞。nanoda 在 Lean 漏掉的位置做了检查，却没有验证投影节点中的类型名称。这个问题已提前一周修复，只是原证明恰好同时绕过了两套实现。
这不是“独立检查无用”，恰恰说明独立实现不能只换一种语言重写同样假设。Lean 团队计划把 nanoda 纳入默认检查流程，并增加内核不变量测试。真正可靠的验证链需要不同实现、针对元编程入口的模糊测试，以及能够保存和重放异常证明的回归库。
关键事实
- 发现时间：2026 年 7 月 28 日提交最小复现，修复补丁约一小时后推送
- 触发条件：需要通过元编程直接构造内核声明，普通前端会拒绝相关非法项
- 实际影响：可让 Lean 接受无公理的
False证明，破坏内核健全性 - 修复状态：Lean PR #14577 已合并，新补丁版本已经发布
OC 判断
先别把“AI 找到证明漏洞”写成数学突破。这里有价值的是，AI 生成的大量非常规项正在扩大证明检查器的输入空间，过去极少有人手写的边缘结构会更频繁地撞向内核。证明助手需要像编译器和解析器一样，把对抗性生成、差分检查和崩溃样本回归当成常规工程。
为什么重要
- 对研究者：重要结果应使用更新后的工具链，并由独立内核重新检查导出的证明对象。
- 对开发者：元编程接口接近可信边界，权限和审计标准应高于普通 tactic 代码。
- 对 AI 数学团队：模型输出“通过检查”仍不等于数学事实，需要记录具体内核版本与检查链。
评论
围绕这篇文章补充信息、提出问题或分享观察。