Lean 内核健全性漏洞 #14576 事后分析
来源：leodemoura.github.io — 2026-08-01
📋 概述
Leonardo de Moura 发布了对 Lean 内核健全性漏洞 #14576 的事后分析。该漏洞于 7 月 27 日那周被报告并修复。起因是 7 月 25 日 Ramana Kumar 发布了一个借助 AI 生成的、关于哥德巴赫猜想的“反证”仓库——它并非有效证明，而是利用了内核处理嵌套归纳类型时的缺陷。修复在报告一小时内完成并已发布补丁版本。
🔑 核心要点
- Ramana Kumar 发布的 AI 辅助“哥德巴赫猜想反证”实际利用了内核处理嵌套归纳类型的 bug
- 7 月 28 日 Kiran Gopinathan 将其归结为对 False 的小证明并打开 issue #14576
- 团队在报告一小时内推送修复（#14577），Joachim Breitner 审查后合入
- Bug 成因：消除带幻影参数的嵌套出现时，参数消失从而逃过类型检查
💡 金句
它不是有效证明，因为它利用了内核在处理嵌套归纳类型时的缺陷。
👍 0
👎 0
← 返回 Lobsters 首页