考拉兹猜想，这个由德国数学家洛塔尔·考拉兹在1937年提出的数学难题，至今仍未被彻底破解。该猜想断言，任意一个正整数经过特定规则的反复运算后，最终都会归结为1。具体规则为：若数字为偶数，则除以2；若为奇数，则乘以3再加1。尽管表述简单，但无数数学家和爱好者尝试证明或推翻这一猜想，均未取得突破性进展。
以数字6为例，其运算过程如下：6是偶数，除以2得到3；3是奇数，乘以3加1得到10；10是偶数，除以2得到5；5是奇数，乘以3加1得到16；16依次除以2得到8、4、2，最终归为1。整个路径为：6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1。这一过程看似简单，但当数字增大时，运算路径会变得极其复杂，甚至无法预测。
近日，一场围绕考拉兹猜想的“风波”在数学和计算机领域引发关注。7月25日，形式化验证专家Ramana Kumar在GitHub上发布了一个项目，声称借助AI在Lean定理证明辅助系统中完成了对考拉兹猜想的推翻。该项目并未提供具体反例整数，而是通过代码证明“存在一个无法到达1的数”。Lean是一款支持用户将数学公式和逻辑编写成程序，并由计算机验证证明准确性的工具，其内核会检查类型与逻辑一致性。
然而，这一“突破”很快被揭穿。Ramana Kumar在审查反驳内容时发现，相关方法存在严重漏洞，甚至能让Lean无条件接受“False”这一假命题。这意味着，原本被认为严谨的证明过程实际上存在逻辑缺陷，无法作为反驳考拉兹猜想的依据。形式化验证研究者Kiran Gopinathan将问题简化为小型复现代码，并于7月28日向Lean开发团队报告了这一漏洞。
漏洞的核心在于Lean内核处理“嵌套归纳类型”时的缺陷。具体来说，内核有时会忽略“幽灵类型参数”——即不直接出现在数据结构组件中的参数，导致错误参数逃过验证。Lean开发者Leonardo de Moura承认，问题源于内核实现未完成应有的检查。这一漏洞不仅影响了考拉兹猜想的证明，还可能对其他依赖Lean的数学研究造成潜在风险。
Lean团队在收到报告后迅速响应，仅约1小时便创建了修复拉取请求，并于7月28日发布Lean 4.32.2版本，彻底解决了这一问题。此次事件再次凸显了形式化验证工具的重要性——尽管计算机辅助证明能大幅提高严谨性，但工具本身的漏洞也可能导致错误结论。对于考拉兹猜想而言，这场“乌龙”证明并未带来实质性进展，但为数学和计算机领域提供了一个宝贵的教训：在追求真理的道路上，严谨与审慎永远不可或缺。
