arXiv 论文：Lean 验证过了不等于证明成立，OpenAI 纳维–斯托克斯的形式化与原证明对不上
10 月 6 日的 arXiv 论文《Navier-Stokes lost in translation》（Bastounis / Circelli / Hansen）指出：让 AI 把自然语言证明翻成 Lean、再由 Lean 机械验证，并不能说明原来的自然语言证明是对的。原因是「消解自然语言数学文本里的歧义」在可解性复杂度层级里位于 SCI = ∞，比停机问题（SCI = 1）还难，因此不存在能保证忠实翻译的算法——Lean 通过只证明被形式化的那条命题。
论文给出的实例里包括 OpenAI 公布的那份纳维–斯托克斯爆破证明：Lean 形式化与自然语言论文的论证并不对应。例如论文 Lemma 8.6 要的是 m+4 阶导数估计，对应 Lean 定理要的是 m+5 阶；压力通量界(10.19) 的 Lean 版本还多依赖一个 A_R。论文配图显示，GPT-6 Astra Ultra 在被追问时自己也承认这两处「翻译不忠实」。
作者的结论是这类 AI 生成的数学成果应接受与其他证明相同的同行评审。对本站 9 月 8 日收录的纳维–斯托克斯条目而言，这是一份外部反驳——但反驳的对象是「自然语言证明与 Lean 证明的对应关系」，不是 Lean 形式化本身，后者目前仍被广泛认为有效。
核验记录
arXiv abs 页直读 200，citation_date 与 citation_online_date 均为 2026/10/06；论文正文经 arXiv HTML 版（arxiv.org/html/2610.08144v1，628,418 字节）直读，两处具体不符（Lemma 8.6 的 m+4 → m+5、式 (10.19) 多一个 A_R）与配图（该版 Figure 3，GPT-6 Astra Ultra 承认翻译不忠实）均取自 HTML 版原文。配图裸请求与带站内 Referer 双 200 / JPEG 397,626 字节。论文口径是「Lean 形式化仍有效，受质疑的是它与自然语言证明的对应关系」——本站正文照此写，未替论文放大结论。本机未能直读 openai.com 官方页面（SSL EOF），故正文不引其自述。
← 上一篇TII 把 270M 的 Falcon OCR 适配成阿拉伯语：真实文档准确率 81.9%，仅次 Gemini 3.5 Flash下一篇 →斯坦福开源 OpenWAM：把世界动作模型拆成可组合的程序，LIBERO-Long 迁移成功率升到 97.8%