AI 热点快报：AI 辅助"反证"考拉兹猜想，意外暴露 Lean 内核 Soundness Bug（2026-08-02）
事件与背景
7 月 25 日，Ramana Kumar 发布了一个仓库，声称用 AI 辅助构造出考拉兹猜想的”无 sorry 反证”——考拉兹猜想是数学界最著名的未解问题之一，如果”反证”成立将是世纪级新闻。然而 7 月 28 日，Kiran Gopinathan 将其约简为一个极小的 False 证明并开出 issue #14576：这个”反证”并非数学突破，而是利用了 Lean 内核处理嵌套归纳类型时的 soundness bug，可以让内核接受一个 False 的证明。Lean 团队在报告后一小时内推送修复（PR #14577，Joachim Breitner 审查后合并），8 月 1 日，Lean 联合创始人 Leonardo de Moura 发布完整复盘。
关键细节：bug 只可通过元编程（直接把归纳声明发给内核）触达，前端会拦截错误类型，因此是实现缺陷而非元理论漏洞。更值得警惕的是，独立检查器 nanoda（ammkrn/nanoda_lib，Chris Bailey 用 Rust 实现的 Lean 独立内核）也没拦住——它漏检了投影节点的类型名，这是两个实现各自独立的不同 bug。目前 nanoda 的修复已合并一周，官方内核修复也已发布补丁版本。
来源：
- Postmortem for Kernel Soundness Bug #14576（de Moura 博客） — 一手复盘，已验证可访问
- GitHub issue #14576：Kernel accepts wrong-structure projections — 已验证（closed）
- 修复 PR #14577 — 已验证（2026-07-28 合并）
- nanoda：Lean 独立检查器 — 已验证可访问
- Hacker News 讨论（133 分 / 45 评论）
为什么现在重要
1. AI 首次成为”验证器的压力测试者”
过去叙事是”AI 生成的证明需要过验证器才算数”——验证器是信任的终点。这次事件反过来了：AI 辅助构造的证明反过来找到了验证器自身的 bug，且不是拍脑袋的错题，而是能让内核接受 False 的真漏洞。判断：验证器从”裁判”变成了”被 AI 攻击的对象”，形式化验证的信任模型需要补上”验证器自身正确性”这一环。
2. 考拉兹猜想级别的诱饵暴露了 AI 证明的”可信幻觉”
这个假”反证”之所以危险，是因为它看起来完全合理：sorry-free、能通过（有 bug 的）内核、指向一个世纪难题。AI 有能力生成”表面完全规范、实际在钻漏洞”的证明。判断：以后任何人宣称 AI 解决了著名开放问题，第一反应应是”检查验证器有没有 bug”，而不是惊叹。
3. 双 bug 巧合：独立检查并非万无一失，但依然是正解
Lean 内核漏了嵌套归纳类型的参数检查，nanoda 漏了投影节点类型名——两个独立实现各有一个不同的洞，单独用任何一个都会被骗。作者坦言”无法排除模型见过 nanoda 修复报告”的可能性，Joachim Breitner 则提出：这或许正是强模型有能力找到此类 bug 的证据。判断：多检查器策略依然有效（需要两个独立 bug 才能击穿），但必须保证所有检查器都更新到最新版本——‘检查一下’不等于’检查对了’。
4. OpenAI 的 AI 安全模型已参与内核审计
de Moura 在复盘中提到：Daniel Selsam（OpenAI）用专攻网络安全的大模型协助 Lean FRO 审计内核，又发现了其他编程错误（PR #14607 等，均已被 nanoda 捕获并修复）。判断：AI-vs-AI 的审计循环已从演示走向生产——用 AI 找 AI 基础设施的漏洞，正在成为安全团队的标准动作。
5. Lean 生态是所有 AI 数学工作的地基
Lean 已是主流定理证明器，越来越多 AI 数学/Agent 工作以它为落点。这次事件没有推翻任何既有 AI 数学成果，但提醒所有基于 Lean 构建的人：地基自身也需要持续审计。判断：选择形式化验证栈时，“是否有多检查器 + 内核是否被持续模糊测试”应成为评估项。
工程师/产品人今天能做什么
- 立即升级：如果你在用 Lean，把 lean4 升级到包含 #14577 修复的补丁版本，并确认
lean4lean等依赖受影响路径的组件同步更新。 - 跑一遍回归：对仓库中涉及嵌套归纳类型、元编程（
elab/ 自定义 elaborator）的证明重新验证——这是 bug 唯一可触达的路径。 - 启用第二检查器：把 nanoda 纳入 CI，作为独立内核交叉验证；重点确认 nanoda 也是最新版（旧版 nanoda 同样有洞）。
- 审慎对待 AI 生成的证明：团队内部约定——AI 生成的数学证明必须过”官方内核 + 独立内核”双验证，且不得仅凭”通过验证”就宣称正确。
- 关注 Kernel Arena 与 comparator.live：Lean FRO 正在用 Kernel Arena 沉淀回归测试，
comparator.live已默认跑 nanoda——把这类基础设施纳入你的工具链监控。
待观察
- de Moura 明确说”无法排除模型见过 nanoda 报告”——若后续证实训练数据污染，将是一个更严重的安全信号。
- OpenAI 安全模型发现的其他内核 bug 是否还有未公开细节；lean4lean 对归纳类型的验证何时完成（届时可在形式化层面证明内核正确性）。
- 事件会否推动”AI 生成的著名问题解答必须先过双检查器”成为社区惯例——下一次 AI 宣称解决开放问题时，验证协议是否已经就位。