2026年7月，Lean内核发现一个关于嵌套归纳类型处理的健全性漏洞（#14576），该漏洞被用于伪造科拉茨猜想的反证。开发者在一小时内完成修复并发布补丁。漏洞源于内核在消除嵌套类型时，未正确处理幻影参数，导致类型检查失效。

好的，这是根据您的要求，对原文进行的中文重述：

关于Lean内核健全性漏洞#14576的事后分析

2026年7月27日当周，Lean内核发现并修复了一个健全性漏洞（编号#14576）。该漏洞在Zulip及社交媒体上引发了关注。

事件经过

7月25日，Ramana Kumar在AI辅助下发布了一个仓库，其中包含一个无需“sorry”的“反证”，声称推翻了考拉兹猜想。但这并非有效证明，因为它利用了内核在处理嵌套归纳类型时的一个漏洞。7月28日，Kiran Gopinathan将其简化为一个证明“False”的小型证明，并提交了问题报告。我们在收到报告一小时后推送了修复。Joachim Breitner审查并提出了改进建议，随后修复被合并，并发布了新的补丁版本。

该漏洞的具体情况是：当内核消除一个带有参数Ds的归纳类型T下的嵌套出现时，如果这些参数是“幻影参数”（即未在构造器字段中被提及），它们会从生成的辅助类型中消失，从而绕过类型检查。一个类型错误的参数若被置于该位置，可被用来让内核接受一个“False”的证明。此漏洞仅能通过元编程（即直接将归纳声明发送给内核）触发。前端检查会捕获此类类型错误的项。这是一个实现上的漏洞，而非Lean元理论本身的缺陷。

为何nanoda未能发现

原始的考拉兹仓库也通过了旧版nanoda的检查。nanoda是一个用Rust实现的独立Lean内核。令人惊讶的是，这涉及两个不相关的漏洞：官方内核在嵌套归纳类型支持上缺少一项检查；而nanoda虽然检查了那个位置，但未验证投影节点中的类型名称。nanoda的漏洞由Jeremy Chen报告，并在Lean漏洞报告前一周被修复。该“反证”被构造得恰好能让旧版nanoda接受那些内核从未检查的表达式。

Ramana认为时间上的巧合是偶然的，但也不能排除AI模型已看到nanoda报告的可能性。Joachim则提出假设，认为这种巧合是由于能够发现此漏洞的强大模型已经可用。

实际后果是：使用独立内核进行检查仍然有效，因为需要两个不同实现中的两个不同漏洞同时存在。但依赖此方法的用户需要确保两个内核都是最新版本。lean4lean也受此内核漏洞影响，因为它对归纳类型的处理是参考实现的移植。

验证情况

Mario Carneiro的lean4lean项目是对Lean类型论的形式化，并包含内核实现该理论的证明。但这项工作仍在进行中，一致性证明尚未涵盖归纳类型，且待验证的实现也存在与官方内核相同的漏洞。该漏洞本应在尝试完成这部分验证时被发现。

关于移除元编程

讨论中有人建议移除或限制元编程，以使此类攻击无法表达。这种观点是错误的。设计上，解释器就是不可信的。健全性不能依赖于一个不可信的组件拒绝构建错误项。想要提交恶意证明的攻击者也可以直接编写.olean文件或修改内存，这两种方式都能完全绕过解释器。内核必须在其自身进程中独立地拒绝类型错误的声明。这种关注点的分离与隔离，正是证明项的主要优势之一。

Lean FRO（形式化研究与开发团队）的应对措施

• 已为漏洞利用及相关案例添加了回归测试，并纳入Kernel Arena。
• 一个后续的拉取请求（#14582）使内核能够检查嵌套出现的参数是否确实表现为参数，而不仅仅是重新进行类型检查。
• OpenAI的Daniel Selsam协助Lean FRO使用专注于网络安全的AI，在Lean内核中发现了其他编程错误。所有这些错误均已修复，且均能被nanoda捕获。这些漏洞同样只能通过元编程触发。
• 我们还强化了内核的不变量。
• comparator.live现在默认运行nanoda，并且nanoda会每日跟踪，以便在上游修复后保持lean-eval和comparator的更新。
• 我们正在联系并支持能够发现更多漏洞、开发新内核以及从事理论或验证内核工作的专家。

致谢

感谢Joachim Breitner和Sebastian Ullrich对本文的修订和建议。

根据评论内容，主要观点和论据总结如下：

1. 核心事件：Lean内核漏洞被AI利用
- 评论1指出，AI辅助生成的Collatz猜想“反证”利用了Lean内核处理嵌套归纳类型的漏洞（#14576），该漏洞在7月27日当周被报告并修复。
- 评论3强调：不能信任LLM生成的代码，即使它通过了形式化验证器的检查。
- 关键引用："One cannot trust the code produced by an LLM, even if the code is a formal proof passing the verifier."
- 关键引用："It is not a valid proof because it exploits a bug in the kernel's handling of nested inductive types."

2. 对形式化验证系统的信任讨论
- 评论4认为，漏洞并不意外（类似Rust类型检查器也有问题），验证结果应视为“极强保证”而非绝对保证，且漏洞会被严肃对待并快速修复。
- 关键引用："verified results not as an absolute and unbreakable guarantee, just an extraordinarily strong one."
- 评论7批评Lean的意识形态，认为漏洞暴露了严重缺陷，并建议使用更严谨的Metamath系统。
- 关键引用："I'd almost consider the fact soundness bugs are possible as a bug in the ideology."
- 关键引用："Stuff like this just wouldn't happen in Metamath."

3. 对Lean的批评与辩护
- 评论6贬低Lean，称其有Claude贡献，推荐使用Coq或Isabelle。
- 关键引用："Lean has Claude contributions, what do you expect! Use Coq or Isabelle."
- 评论8引用Knuth名言，暗示形式化证明与实际运行存在差距。
- 关键引用："Beware of bugs in the above code; I have only proved it correct, not tried it."

4. 技术细节与改进建议
- 评论5质疑Collatz反证是否应为构造性反例，暗示非构造性证明难以验证。
- 关键引用："Isn't a disproof of the Collatz conjecture easy to check as it should just be a counterexample?"
- 评论9提出：若每个漏洞利用都能直接证明False，则可通过悬赏证明False来增强信任。
- 关键引用："putting a bounty on proving false could increase trust in the validity of verified but obscure Lean proofs."

平衡性总结：
- 支持Lean的视角：漏洞被快速修复，验证系统仍提供极强保证（评论4）。
- 批评Lean的视角：漏洞暴露了系统脆弱性，AI生成代码不可信，建议使用更严谨的替代方案（评论3、6、7）。
- 中立技术讨论：关注漏洞性质、验证方法改进（评论5、9）。