AI 证明考拉兹猜想被确认无效，Lean 系统漏洞致误判

一项借助 AI 完成、声称推翻考拉兹猜想的 Lean 形式化证明被确认无效。考拉兹猜想由德国数学家洛塔尔·考拉兹于 1937 年提出，断言任意正整数经特定迭代最终回到 1，至今未解。形式化验证专家 Ramana Kumar 于 7 月 25 日在 GitHub 发布项目，称用 AI 推翻了该猜想，但未给出具体反例，仅证明“存在无法到达 1 的数”。

Kumar 在审查时发现，相关方法甚至能让 Lean 无条件接受“False”，表明存在漏洞。验证研究者 Kiran Gopinathan 将问题缩减为复现代码，并于 7 月 28 日报告给 Lean 团队。漏洞位于内核处理“嵌套归纳类型”部分，导致忽略“幽灵类型参数”，使错误参数逃过验证。Lean 开发者 Leonardo de Moura 确认问题后，团队约 1 小时后创建修复，并于 7 月 28 日发布 Lean 4.32.2 版本。