Lean内核漏洞：AI竟证伪Collatz猜想
Postmortem for Kernel Soundness Bug #14576
Lean内核近日被曝出一个严重漏洞，导致AI辅助生成的代码成功构造出Collatz猜想的“反证”。该漏洞源于内核在处理嵌套归纳类型时，对幻象参数的检查缺失，使得非法类型参数得以逃逸。尽管独立验证器nanoda也未能拦截，但这是因为两者恰好存在不同的实现缺陷。此次事件并非Lean元理论的漏洞，而是实现层面的问题。修复已迅速上线，团队正通过强化内核不变量、引入AI安全工具以及完善回归测试来加固系统。这一案例再次证明，内核必须独立于不可信的元编程组件，自行拒绝非法声明，这是证明项架构的核心优势。
这种关注点的分离与隔离，正是证明项架构的主要优势之一。
HN 评论区
17- gr_norm
实际后果是：使用独立内核进行验证依然有效，因为这需要在两个不同的实现中同时存在两个独立的漏洞；但依赖此功能的用户需要确保两者都是最新版本。
考虑到连 Rust 这样相对简单的类型检查器偶尔也会出现健全性问题，这类事情并不太令人意外。我认为非常重要的一点是，不要把经过验证的结果视为绝对且不可打破的保证，而应将其视为一种极其强大的保障，其前提是：(1) 健全性问题的潜在范围已被 painstakingly 最小化；(2) 任何已发现的健全性问题都会被高度重视并迅速修复。
- twotwotwo
这个线程提供了一些背景信息。一位证明系统研究人员发现了一些证明系统漏洞，并以一种有趣的方式展示了出来：
https://leanprover.zulipchat.com/#narrow/channel/270676-lean...
一位有数学背景的审稿人（或 LLM）可以迅速识别出这是一个利用漏洞的攻击（实际上是两个漏洞；该攻击特意设计为同时触发另一个证明检查器中的漏洞）。
原帖对此有所提及，但一个自然的后续步骤，除了修复与此漏洞相关的具体 bug 外，还应让一些面向安全的模型尝试在 Lean 中证明 False，或者审查代码中可能存在的非健全步骤、缺失的检查，甚至进行有用的“加固”。目前这项工作正在进行中，并因此产生了相应的 bug 修复。
- dafelst
对于形式化证明系统中的漏洞，这句话似乎非常贴切：
> 警惕上述代码中的 bug；我只证明了它正确，并未实际运行过。
——Knuth, 1977
- michaelfm1211
这让我想起了这个：https://mathoverflow.net/questions/513742/are-we-stuck-with-...
我知道这是一个实现层面的 bug，而非元理论层面的 bug，但我几乎会认为“健全性漏洞可能存在”这一事实本身就是意识形态上的一个 bug，或者至少是一个严重的缺陷。在 Metamath 中，这类事情根本不会发生。在未来 AI 自动生成形式化证明的时代，为什么不让 AI 使用像 Metamath 这样虽然更难但无懈可击的系统呢？
- Gehinnn
是否曾经出现过这样的 bug：它允许证明一个此前无法证明的命题，但用户无法通过直接利用该漏洞来证明 'false'？
如果每一个利用漏洞的证明都能轻易导出 'false'，那么设立一个针对证明 'false' 的赏金，或许能增加人们对那些已验证但晦涩难懂的 Lean 证明有效性的信任。