剑桥团队证明：AI 数学证明通过 Lean 验证也不等于正确
rohanpaul_ai · x · 2026-10-08
arXiv 新论文《Navier-Stokes lost in translation》直击 AI 数学验证的核心漏洞：把自然语言证明自动形式化（autoformalisation）成 Lean 并通过机器验证，并不能说明原始证明是对的。
核心论点：
- 论文以 OpenAI 宣称的 Navier-Stokes 方程解爆破证明为背景，指出 AI 在翻译时可能「悄悄修错」——作者演示了一个聊天机器人把错误的证明翻译成合法的 Lean 证明，错误被自动修正而非保留。
- 消除数学自然语言文本歧义所需的语义忠实翻译，其复杂度位于 Solvability Complexity Index（SCI）层级的最高处（SCI = ∞），即比包括停机问题在内的任何计算问题都难（停机问题 SCI = 1）。
- 结论：不存在能永远忠实翻译的 AI 形式化系统，Lean 验证通过 ≠ 原始论证正确。
论文由 Alexander Bastounis、Fabian Circelli、Anders C. Hansen 撰写，并给出多个 AI 在实践中将自然语言陈述/证明误译入 Lean 的实例。
所属事件:剑桥论文质疑 Lean 验证可信度，直指 OpenAI Navier-Stokes 证明(14 条相关)→
「研究」频道最新
- Cyber Index 方法论详解：三套基准合成，Grok 4.7 与 MiMo-V2.6-Pro 公开版并列 56 分 — ArtificialAnlys · 2026-10-09
- LightOnOCR-3 训练秘辛：用 OCR 参考文本引导逻辑分块 — IgorCarron · 2026-10-09
- LightOnOCR-3 揭示：单一版面模型无法覆盖全部文档类型 — IgorCarron · 2026-10-09
- Text2Sim 用文本生成物理仿真场景，输出可编辑的真物理视频 — erwincoumans · 2026-10-09
- 单张图像重建 3D 场景:Building Rome 项目可见范围外几何也补全 — jonstephens85 · 2026-10-09
- PredActor 用单一扩散策略统一人形机器人运动生成与控制,G1 端侧跑 50Hz — carlosdponx · 2026-10-09