推文

@RJDAIGOGO · 2026-10-09 09:03

学界重磅质疑：OpenAI纳维–斯托克斯证明存在致命翻译偏差，Lean验证不可完全采信 一篇10月6日上线arXiv预印本平台的数学论文，对OpenAI号称“攻克千禧年难题”的纳维–斯托克斯（N-S）有限时间爆破证明提出质疑，直指其证明存在严重“文码不符”问题。 三位权威数学专家Anders C. Hansen（剑桥大学DAMTP，国际顶尖分析与计算数学学者）、Fabian Circelli（剑桥大学DAMTP）、Alexander Bastounis（伦敦国王学院）发表论文《Navier–Stokes lost in translation》，论文指出：OpenAI纳维-斯托克斯（N-S）证明里，自然语言书面证明，和AI转写出来的Lean形式化验证代码存在不匹配；Lean本身机械校验通过，但Lean证明的定理，和论文文字声称要证明的定理不完全是同一个命题。 1、两处不匹配 1. 导数估计：自然语言论文称4阶额外导数足够；对应的Lean形式版本需要5阶导数，Lean证明的是一个更弱的结论。 2. 压力-通量估计：文字版与Lean版本使用的界、论证路径不一样。 论文作者表示，这不直接等同于整个证明彻底作废，但存在翻译失真。AI在把人类可读数学文本翻译成Lean形式语言时，会悄悄修改假设、弱化命题，相当于“证明了另一个定理”，Lean只能保证形式代码内部逻辑自洽，不能保证代码忠实还原原文的数学主张。 2、背景：OpenAI近期所做的两件事 1. 9月8日，OpenAI宣称解决千禧年难题纳维–斯托克斯有限时间爆破，同时放出自然语言论文+Lean形式化证明； 2. 近期一次性发布722篇AI生成数学论文（网传“700篇”是近似说法），引发学界大讨论。 3、小结 Lean的作用是检查形式代码内部逻辑有没有矛盾，它不会自动核验形式代码化的命题，是不是克雷数学研究所原版千禧问题。 AI自动形式化翻译时，可能发生“翻译走样”，出现Lean验证通过，但证明的是另一个结论，这就是论文所说的认识论问题。 OpenAI尚未正式回应这篇arXiv论文指出的两处不一致。相关证明仍在同行评审阶段，克雷数学研究所并没有认定N-S问题已经被解决。

曝光 1061 · 评论 0 · 点赞 3 · 书签 0