**AI 辅助“推翻”考拉兹猜想失败，Lean 4.32.2 修复内核漏洞**

> IT之家 8 月 4 日消息，科技媒体 Gigazine 昨日（8 月 3 日）发布博文，<strong\>报道称一项借助 AI 完成、声称推翻考拉兹猜想的 Lean 形式化证明被确认无效。</strong\></p\>IT之家注：考拉兹猜想（又称奇偶归一猜想 / 3n+1 猜想）由德国数学家洛塔尔 · 考拉兹（Lothar Collatz）于 1937 年提出，是一个表述极其简单但至今未解的数学难题，<strong\>断言任意正整数在经过特定规则的反复迭代后，最终都一定会回到 1。</strong\></p\>其计算规则是对于任意一个正整数 n：</p\><ul class="medium-size list-paddingleft-2"\><li\>如果 n 是偶数，就把它除以 2（n ÷ 2）。</p\></li\><li\>如果 n 是奇数，就把它乘以 3 再加 1（3n + 1）。</p\></li\><li\>得到新数字后，重复上述步骤，直到结果变为 1。</p\></li\></ul\>以数字 6 为例：</p\><ul class="medium-size list-paddingleft-2"\><li\>6 是偶数，除以 2 得到 3</p\></li\><li\>3 是奇数，乘以 3 加 1 得到 10</p\></li\><li\>10 是偶数，除以 2 得到 5</p\></li\><li\>5 是奇数，乘以 3 加 1 得到 16</p\></li\><li\>16 依次除以 2 得到 8、4、2、1</p\>最终路径为：6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1。</p\></li\></ul\>形式化验证专家 Ramana Kumar 于 7 月 25 日在 GitHub 发布项目，<strong\>最初</strong\><strong\>称借助 AI 推翻了考拉兹猜想。</strong\>项目没有给出一个具体反例整数，只是在 Lean（定理证明辅助系统）中证明“存在一个无法到达 1 的数”。</p\><img src="https://img.ithome.com/newsuploadfiles/2026/8/afd2b986-4246-4e58-a314-3d4a572c4bb3.png" w="560" h="211" data-weibo="0" data-vmark="3069" class="no-alt-img"\></p\>Lean 是一款定理证明辅助系统，支持用户将数学公式和逻辑编写成程序，并由计算机验证证明的准确性。用户编写的 Lean 代码会把数学命题和证明写成可检查的程序，并由内核验证类型与逻辑一致性。</p\>不过他随后在审查反驳内容时发现，相关方法甚至能让 Lean 无条件接受“False”（代表假命题），因此目前相关代码并不能反驳考拉兹猜想。</p\>形式化验证研究者 Kiran Gopinathan 将问题缩减为小型复现代码，并于 2026 年 7 月 28 日报告给 Lean 开发团队。</p\>漏洞位于内核处理“嵌套归纳类型”部分，导致有时候会忽略“幽灵类型参数”（即不直接出现在数据结构组件中的参数），导致原本应该被判定为错误的参数逃过了验证。Lean 开发者 Leonardo de Moura 表示问题在于内核实现未完成应有的检查。</p\>Lean 团队在收到报告约 1 小时后创建修复拉取请求，于 7 月 28 日发布 Lean 4.32.2 版本，修复了这个问题。</p\>

**来源信息**
- **来源**：IT之家（RSS）
- **分类**：ai-models
- **发布时间**：2026-08-04 13:35（北京时间）
- **原文**：[打开原文](https://www.ithome.com/0/985/448.htm)

AI 辅助“推翻”考拉兹猜想失败，Lean 4.32.2 修复内核漏洞 > <p data-vmark="e93f"\>IT之家 8 月 4 日消息，

原帖