AI 辅助“推翻”考拉兹猜想失败，Lean 4.32.2 修复内核漏洞

一项借助AI完成、声称推翻考拉兹猜想的Lean形式化证明被确认无效。该证明由形式化验证专家Ramana Kumar于7月25日在GitHub发布，但后续审查发现，Lean定理证明辅助系统存在内核漏洞，导致相关代码无法作为有效反驳。

考拉兹猜想又称“3n+1猜想”，由德国数学家洛塔尔·考拉兹于1937年提出。其规则极为简单：对任意正整数n，若为偶数则除以2，若为奇数则乘以3再加1，反复迭代后最终都会回到1。尽管规则简单，该猜想至今未被证明或推翻。

Ramana Kumar的项目并未给出具体反例整数，而是在Lean中证明“存在一个无法到达1的数”。然而，他在审查反驳内容时发现，相关方法甚至能让Lean无条件接受“False”这一假命题，因此该证明并不成立。

随后，形式化验证研究者Kiran Gopinathan将问题缩减为小型复现代码，并于7月28日报告给Lean开发团队。漏洞位于内核处理“嵌套归纳类型”的部分，导致有时会忽略“幽灵类型参数”，使原本应判定为错误的参数逃过验证。

Lean开发者Leonardo de Moura表示，问题在于内核实现未完成应有的检查。Lean团队在收到报告约1小时后创建修复拉取请求，并于同一天发布Lean 4.32.2版本，修复了这一漏洞。

这一事件凸显了形式化验证工具自身可靠性的重要性。AI辅助数学证明虽然潜力巨大，但依赖的底层系统若存在缺陷，结论便可能失去依据。未来，加强定理证明器内核的验证与测试，将有助于避免类似问题。