Lean 内核漏洞击穿 AI 数学证明

IT之家 8 月 4 日消息，科技媒体 Gigazine 昨日（8 月 3 日）发布博文称，一项借助 AI 完成、声称推翻考拉兹猜想的 Lean 形式化证明已被确认无效。

IT之家注：考拉兹猜想（又称奇偶归一猜想 / 3n+1 猜想）由德国数学家洛塔尔·考拉兹（Lothar Collatz）于 1937 年提出。它是一个表述极其简单、但至今仍未解决的数学难题，断言任意正整数经过特定规则的反复迭代后，最终都一定会回到 1。

如果 n 是偶数，就把它除以 2（n ÷ 2）。

如果 n 是偶数，就把它除以 2（n ÷ 2）。

如果 n 是奇数，就把它乘以 3 再加 1（3n + 1）。

如果 n 是奇数，就把它乘以 3 再加 1（3n + 1）。

得到新数字后，重复上述步骤，直到结果变为 1。

得到新数字后，重复上述步骤，直到结果变为 1。

16 依次除以 2，得到 8、4、2、1。最终路径为：6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1。

最终路径为：6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1。

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

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

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

形式化验证研究者 Kiran Gopinathan 将问题缩减为一段小型复现代码，并于 2026 年 7 月 28 日将其报告给 Lean 开发团队。

漏洞位于内核处理“嵌套归纳类型”的部分，导致系统有时会忽略“幽灵类型参数”（即不直接出现在数据结构组件中的参数），使原本应该被判定为错误的参数逃过验证。Lean 开发者 Leonardo de Moura 表示，问题在于内核实现没有完成应有的检查。

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

广告声明：文内含有的对外跳转链接（包括但不限于超链接、二维码、口令等形式），用于传递更多信息、节省甄选时间，结果仅供参考。IT之家所有文章均包含本声明。

软媒旗下网站：IT之家、最会买 - 返利返现优惠券、iPhone之家、Win7之家、Win10之家、Win11之家

软媒旗下软件：软媒手机 APP 应用、魔方、最会买、要知