AI生成伪证明攻破Lean内核，官方复盘可靠性Bug
AlexKontorovich · x · 2026-08-03
Lean定理证明器核心开发者 Leonardo de Moura 发布了关于内核可靠性 Bug (#14576) 的详细复盘报告。
事件经过
7月25日，Ramana Kumar 发布了一个在 AI 辅助下生成的无 sorry 代码库，声称“证伪”了考拉兹猜想。这实际上利用了 Lean 内核处理嵌套归纳类型时的漏洞。随后 Kiran Gopinathan 将其简化为直接证明 False 的极简代码并提交了 Issue。官方在一小时内完成修复并合并。
Bug 原理
当内核在处理带有幻影参数的嵌套归纳类型时，参数会从生成的辅助类型中消失从而逃逸类型检查。攻击者可在该位置传入类型不匹配的参数，骗过内核接受 False 的证明。该漏洞仅能通过元编程直接向内核发送声明触发，前端检查会拦截此错误项，属于实现 Bug 而非 Lean 元理论缺陷。
外部检查器为何失守
该伪证明最初甚至通过了 Rust 实现的独立外部检查器 nanoda。原因是存在两个不相关的 Bug：官方内核漏掉了嵌套检查，而 nanoda 虽检查了该处，却在投影节点的类型名称验证上存在疏漏。
「研究」频道最新
- AI 破解数学难题，人类智力资本正被推向极限 — SNad2020 · 2026-08-03
- 本周信息检索前沿论文：Meta、YouTube、腾讯共探 RAG 与生成式推荐 — _reachsumit · 2026-08-03
- AI 居里温度预测器使用量破 6000，加速磁性材料筛选 — CatAstro_Piyush · 2026-08-03
- Kimi K3 深度技术解析：2.78万亿参数架构与训练机制 — imrancoder · 2026-08-03
- MIT与哈佛新研究：LLM尚不具备自主科学发现能力 — davidmanheim · 2026-08-03
- 经典论文：用机器学习预测算法运行时间，Hutter 等 2014 年研究 — tomssilver · 2026-08-03