Lean内核中发现了一个严重的健全性漏洞（bug #14576），该漏洞允许类型不匹配的参数绕过类型检查系统。[1]这一bug存在于内核对嵌套归纳类型的处理机制中，只能通过metaprogramming访问，需要直接向内核发送归纳类型声明才能触发。[1]
事件的曝光始于7月25日，当时Ramana Kumar发布了包含虚假Collatz猜想证明的代码库。[1]三天后的7月28日，Kiran Gopinathan将其进一步化简为False证明，并正式开启issue #14576。[1]内核开发团队对此反应迅速，在报告后一小时内推送了修复补丁。[1]随后团队进行了多项后续加固工作，推送了包括#14582、#14607、#14608、#14609、#14613、#14615、#14616、#14621、#14631和#14632在内的多个修复PR。[1]
此外，OpenAI的Daniel Selsam协助内核团队利用AI安全专家发现了其他内核编程错误。[1]值得注意的是，Rust实现的独立内核nanoda中存在相关但不同的bug，该bug由Jeremy Chen报告并在Lean官方bug报告前一周被修复。[1]
A critical soundness vulnerability in the Lean kernel was discovered on July 25, exposing a flaw in how the system handles nested inductive types [1]. The bug surfaced through an AI-assisted fake proof of the Collatz conjecture that Ramana Kumar published [1]. On July 28, Kiran Gopinathan reduced the issue to a proof of False and opened issue #14576, revealing that ill-typed parameters could circumvent type validation, allowing unsound theorems to be accepted by the system [1].
The Lean kernel team responded swiftly, deploying a fix within one hour of the report through pull request #14577 [1]. The vulnerability required direct metaprogramming access to send inductive type declarations to the kernel, limiting its exploitability surface [1]. Following the initial patch, the team implemented multiple hardening measures across subsequent pull requests #14582, #14607, #14608, #14609, #14613, #14615, #14616, #14621, #14631, and #14632 [1]. Daniel Selsam from OpenAI assisted the team by working with AI safety experts to identify additional kernel programming errors [1].
A related but distinct bug was discovered independently in nanoda, a Rust implementation of a separate kernel, by Jeremy Chen and was repaired one week before the Lean vulnerability became public [1].