就在今年8月4日，科技媒体Gigazine披露了一则引人关注的消息：一项借助AI完成、声称推翻考拉兹猜想（Collatz conjecture）的Lean形式化证明，最终被确认无效。不过，这一事件同时意外地暴露了Lean自身的一个内核漏洞，也算得上是因祸得福。

先来简要回顾一下考拉兹猜想。它也被称为奇偶归一猜想或3n+1猜想，由德国数学家洛塔尔·考拉兹于1937年提出。这个猜想的表述极为简单，但至今仍无人能完全证明：对于任意一个正整数，按照特定规则反复迭代，最终一定会到达1。规则只有两条：如果n是偶数，就除以2；如果n是奇数，则乘以3再加1。得到新数后重复操作，直到变成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。

回到这次事件。形式化验证专家Ramana Kumar于7月25日在GitHub上发布了一个项目，最初声称借助AI成功推翻了考拉兹猜想。需要注意的是，他并未给出一个具体的反例整数，而是通过Lean（定理证明辅助系统）证明了“存在一个无法到达1的数”。Lean的工作原理，简单来说，就是将数学公式和逻辑编写成程序，由计算机内核来验证证明的正确性——用户编写的代码会把命题和证明转化为可检查的形式，内核则负责检查类型与逻辑是否一致。

但问题很快浮出水面。Kumar在审查自己提出的反驳内容时发现，这套方法甚至能让Lean无条件接受“False”（假命题）。换句话说，代码本身存在漏洞，根本无法作为反驳考拉兹猜想的有效证据。随后，形式化验证研究者Kiran Gopinathan将问题精炼成一个小型复现代码，并于7月28日报告给了Lean开发团队。

漏洞究竟出在哪里？关键在于内核处理“嵌套归纳类型”时，有时会忽略所谓的“幽灵类型参数”——那些不直接出现在数据结构组件中的参数。结果，原本应该被判定为错误的参数就这样逃过了验证。Lean的开发者Leonardo de Moura承认，问题的根源在于内核实现没有完成应有的检查。

修复速度倒是相当迅速。Lean团队在收到报告后大约1小时便创建了修复拉取请求，并于7月28日发布了Lean 4.32.2版本，彻底堵上了这个漏洞。至于考拉兹猜想，它依然安然无恙，静静地等待着下一个挑战者前来破解。