新论文质疑 OpenAI Navier-Stokes 证明：Lean 验证≠自然语言证明正确
miniapeur · x · 2026-10-08
arXiv 论文《Navier-Stokes lost in translation》直接挑战 OpenAI 宣布的 Navier-Stokes 爆解证明：作者 Bastounis、Circelli、Hansen 展示了该 AI 形式化证明的 Lean 版本与自然语言原证明并不对应。
- 论文指出，AI autoformalisation（把自然语言数学文本翻译成 Lean 等形式语言再机械验证）并不能保证原自然语言论证正确。
- 核心论点：消解数学自然语言中的歧义在可解性复杂度指数（SCI）层级中处于任意高位（SCI=∞），即语义忠实的自动形式化比包括停机问题在内的任何计算问题都难。
- 作者给出多个实际 AI 误译案例，导致 NL 证明与其 Lean「验证」之间出现不匹配，OpenAI 公布的 Navier-Stokes 证明即为例证之一。
所属事件:剑桥论文质疑 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