近日，科技媒体Gigazine报道了一项关于考拉兹猜想的研究进展。考拉兹猜想，又称奇偶归一猜想或3n+1猜想，由德国数学家洛塔尔·考拉兹于1937年提出，是一个至今未解的数学难题。该猜想断言，任意正整数经过特定规则的反复迭代后，最终都会回到1。规则是：如果n是偶数，则除以2；如果n是奇数，则乘以3再加1，重复此过程直到结果为1。

7月25日，形式化验证专家Ramana Kumar在GitHub发布项目，最初声称借助AI推翻了考拉兹猜想。项目没有给出具体反例整数，而是在Lean（定理证明辅助系统）中证明“存在一个无法到达1的数”。Lean支持用户将数学公式和逻辑编写成程序，并由计算机验证证明的准确性。然而，Kumar在审查反驳内容时发现，相关方法甚至能让Lean无条件接受“False”，因此相关代码并不能反驳考拉兹猜想。

形式化验证研究者Kiran Gopinathan将问题缩减为小型复现代码，并于7月28日报告给Lean开发团队。漏洞位于内核处理“嵌套归纳类型”部分，导致有时候会忽略“幽灵类型参数”，导致原本应该被判定为错误的参数逃过了验证。Lean开发者Leonardo de Moura表示问题在于内核实现未完成应有的检查。Lean团队在收到报告约1小时后创建修复拉取请求，于7月28日发布Lean4.32.2版本，修复了这个问题。