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 虽检查了该处，却在投影节点的类型名称验证上存在疏漏。
「研究」频道最新
- Optuna 作者秋叶哉：花3亿日元调2个超参的时代，BO/HPO 还有何用武之地 — Stefania_druga · 2026-10-16
- 学者争论：AI 将超越人类做科学，欧洲躲不开只能用别人的 — teortaxesTex · 2026-10-16
- 上海 AI Lab 提出 SERO：用可执行 Oracle 续跑训练长程智能体强化学习 — Shanghai-AI-Laboratory · 2026-10-16
- 清华联手高德发布 OmniVerifier-C1：把二元验证器升级为细粒度打分 — Bowei Liu · 2026-10-16
- 阿里开源 MAI-Gym：移动与桌面 GUI Agent 评测加强化学习训练一体化平台 — Tongyi-MAI · 2026-10-16
- 北大发布 SimForcing：把仿真运动先验蒸馏进真实机器人世界模型 — PekingUniversity · 2026-10-16