AI辅助考拉兹猜想证明被证伪，Lean修复内核漏洞

近日，一项借助AI辅助完成的数学证明引发了广泛关注，但最终被证实无效。这项声称推翻考拉兹猜想（又称3n+1猜想）的Lean形式化证明，在审查过程中被发现存在严重漏洞，不仅无法证明猜想，甚至可能导致系统接受错误的命题。

考拉兹猜想由德国数学家洛塔尔·考拉兹于1937年提出，其表述极为简单：对于任意正整数n，若为偶数则除以2，若为奇数则乘以3加1，重复此过程，最终总能回到1。尽管规则简单，但至今无人能够证明或推翻它，成为数学界著名的未解难题。

形式化验证专家Ramana Kumar于7月25日在GitHub发布项目，声称借助AI推翻了考拉兹猜想。该项目并未给出具体的反例整数，而是在Lean定理证明辅助系统中证明了“存在一个无法到达1的数”。Lean是一种支持用户将数学公式和逻辑编写成程序，并由计算机验证证明准确性的系统。用户编写的Lean代码将数学命题和证明转化为可检查的程序，由内核验证类型与逻辑一致性。

然而，Kumar在审查反驳内容时发现，相关方法存在严重缺陷，甚至能让Lean无条件接受“False”（代表假命题）。这意味着该证明方法本身并不可靠，无法作为反驳考拉兹猜想的有效证据。形式化验证研究者Kiran Gopinathan将问题缩减为小型复现代码，并于7月28日报告给Lean开发团队。

漏洞定位在内核处理“嵌套归纳类型”的部分，导致有时会忽略“幽灵类型参数”——即不直接出现在数据结构组件中的参数，使得原本应被判定为错误的参数逃过了验证。Lean开发者Leonardo de Moura表示，问题在于内核实现未完成应有的检查。Lean团队在收到报告约1小时后创建修复拉取请求，并于7月28日发布Lean 4.32.2版本，修复了该问题。

这一事件凸显了形式化验证在数学研究中的重要性，同时也提醒我们，AI辅助证明虽然潜力巨大，但仍需严格验证。Lean团队的快速响应和修复，展示了开源社区在维护工具可靠性方面的效率。对于考拉兹猜想而言，这一挑战虽失败，但过程本身为形式化验证领域提供了宝贵经验。