13:41IT之家（博客/媒体）
推荐理由：Ramana Kumar 用 AI 声称推翻考拉兹猜想，结果败给 Lean 内核漏洞，4.32.2 已修复。
考拉兹猜想
共 1 条相关 AI 资讯
8月4日
13:41
7月25日，Ramana Kumar 在 GitHub 发布项目，声称借助 AI 在 Lean 中推翻了考拉兹猜想，但未给出具体反例整数，只证明了“存在一个无法到达 1 的数”。审查后他发现该方法可让 Lean 无条件接受“False”，相关证明因此无效。7月28日，Kiran Gopinathan 将问题缩减为小型复现代码并报告给 Lean 开发团队，漏洞出在内核处理“嵌套归纳类型”时忽略了“幽灵类型参数”。Lean 团队约1小时后创建修复拉取请求，并于当天发布 4.32.2 版本修复该内核漏洞。