新论文：Lean 验证通过≠自然语言证明正确，AI 数学形式化有根本缺陷
natanielruizg · x · 2026-10-08
剑桥学者 Bastounis、Circelli 与 Hansen 发表论文《Navier-Stokes lost in translation》，直接质疑当前流行的 "autoformalisation" 验证流程——包括 OpenAI 宣称的 Navier-Stokes 方程爆破证明所用的方法。
核心论点：AI 把自然语言数学文本翻译成 Lean 等形式语言后，形式化证明虽可机械验证，但这并不能保证原自然语言论证正确，因为翻译本身可能语义失真。
作者进一步给出理论结果：消解数学自然语言中的歧义（语义忠实翻译的前提）在 Solvability Complexity Index (SCI) 层级中处于任意高位（SCI = ∞），即这一任务比包括停机问题（SCI = 1）在内的任何可计算问题都更难。论文还给出多个 AI 在实践中把自然语言陈述和证明错误翻译进 Lean 的实例，导致自然语言论证与形式化版本不匹配。
所属事件:剑桥论文质疑 Lean 验证可信度，直指 OpenAI Navier-Stokes 证明(14 条相关)→
「研究」频道最新
- 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
- 研究称持续学习无需 on-policy,正确的 off-policy 训练同样有效 — AdtRaghunathan · 2026-10-09