注：考拉兹猜想由德国数学家洛塔尔 · 考拉兹于 1937 年提出，是一个表述极其简单但至今未解的数学难题，

　　形式化验证专家 Ramana Kumar 于 7 月 25 日在 GitHub 发布项目，最初称借助 AI 推翻了考拉兹猜想。项目没有给出一个具体反例整数，只是在 Lean中证明“存在一个无法到达 1 的数”。

　　Lean 是一款定理证明辅助系统，支持用户将数学公式和逻辑编写成程序，并由计算机验证证明的准确性。用户编写的 Lean 代码会把数学命题和证明写成可检查的程序，并由内核验证类型与逻辑一致性。

　　不过他随后在审查反驳内容时发现，相关方法甚至能让 Lean 无条件接受“False”，因此目前相关代码并不能反驳考拉兹猜想。

　　漏洞位于内核处理“嵌套归纳类型”部分，导致有时候会忽略“幽灵类型参数”，导致原本应该被判定为错误的参数逃过了验证。Lean 开发者 Leonardo de Moura 表示问题在于内核实现未完成应有的检查。

　　Lean 团队在收到报告约 1 小时后创建修复拉取请求，于 7 月 28 日发布 Lean 4.32.2 版本，修复了这个问题。