Lean 内核漏洞复盘：AI 辅助生成 Collatz 猜想“伪证”始末

Lean 交互式定理证明器的开发团队近期发布了一份关于内核健全性漏洞 #14576 的详细复盘报告。该漏洞引发了社区的广泛关注，因为它被用于生成一份看似无懈可击的 Collatz 猜想“证伪”证明。具体而言，研究员 Ramana Kumar 在 AI 的辅助下，利用 Lean 内核在处理嵌套归纳类型时的逻辑缺陷，构建了一份不包含任何手动不可靠公理的“虚假证明”。尽管该证明在语法上符合 Lean 的规则，但它实际上是通过内核 Bug 证明了逻辑谬误“False”。随后，Kiran Gopinathan 成功将这一复杂的数学攻击简化为最小化的反例，协助团队定位并修复了问题。此事件不仅展示了 AI 在探索逻辑边界方面的潜力，也再次提醒形式化验证领域，核心推理引擎的健壮性是数学真理的最后一道防线。

事件分析

💡 核心观点：AI 不仅是编程助手，更能充当高级“模糊测试器”，挖掘形式化工具深处的逻辑盲区。