新论文质疑 OpenAI Navier-Stokes 证明：Lean 验证通过≠自然语言证明正确
pmddomingos · x · 2026-10-08
Pedro Domingos 转发了一篇 arXiv 论文《Navier-Stokes lost in translation》，作者为 Alexander Bastounis、Fabian Circelli 和 Anders C. Hansen。论文指出：AI autoformalisation（将自然语言数学文本翻译为 Lean 等形式语言再做机器验证）可能无法为原始自然语言论证提供可信保证。
- 论文点名 OpenAI 宣称的 Navier-Stokes 方程 blow-up 证明即属于此类验证流程。
- 核心论证：对数学自然语言文本做语义忠实的翻译需要消解歧义，而该问题在 Solvability Complexity Index（SCI）层级中处于任意高的位置（SCI = ∞），通俗地说比停机问题等任何可计算问题都难。
- 作者给出多个 AI 在实践中把自然语言陈述/证明错译成 Lean 的实例，导致验证过的形式化版本与原始自然语言论证不匹配。
- 结论：形式验证通过并不等于自然语言证明正确，对 AI 生成数学证明的验证方法论提出根本性质疑。
所属事件:剑桥论文质疑 Lean 验证可信度，直指 OpenAI Navier-Stokes 证明(14 条相关)→
「模型」频道最新
- Artificial Analysis 成立 Cyber Index Alliance，IBM、NVIDIA、Vercel 已加入 — ArtificialAnlys · 2026-10-09
- Cyber Index 方法论详解：三套基准合成，Grok 4.7 与 MiMo-V2.6-Pro 公开版并列 56 分 — ArtificialAnlys · 2026-10-09
- Daybreak Blue 相对公开版提升最大的基准：安全拒绝最多的 CyberGym-E2E — ArtificialAnlys · 2026-10-09
- Cyber Index 单任务成本对比：GPT-6 Sol 信任版 $1.77，Grok 4.7 高达 $11.67 — ArtificialAnlys · 2026-10-09
- GPT-6 Sol 信任访问版登顶 Cyber Index，单任务成本仅 Grok 的 1/6 — ArtificialAnlys · 2026-10-09
- LightOnOCR-3 引发热议：文档解析模型被认为「离谱地强」 — IgorCarron · 2026-10-09