OpenAI称解出纳维—斯托克斯难题：形式化证明仍不等于定论

OpenAI于2026年9月8日发布的说明 提出了一份纳维—斯托克斯存在性与光滑性问题的候选解答：一个内部AI系统构造出初始光滑且静止的三维流体，使其在光滑外力作用下于有限时间形成奇点，同时保持有限能量。该页面还给出约一万名并行代理搜索约88小时、GPT-6 Astra再用约17小时完成Lean形式化与验证的时间线。

直接回答“OpenAI的纳维—斯托克斯证明是真的吗”：它是真实公开、可以检查的重大证明主张，但目前不能等同于数学界已经确认千禧年难题解决。《Nature》对9月8日发布的报道 确认其核心主张是方程可能在有限时间失去光滑性；而 《国家报》9月9日的调查 指出，当时尚无外部科学家完成独立验证。因此，更准确的表述仍是“OpenAI声称给出了解答”。

候选证明究竟声称解决了什么

纳维—斯托克斯方程描述水、空气等流体的运动。千禧年问题不是问工程师能否近似计算一次飞行或一段管道中的流动，而是问三维不可压缩流体从光滑状态出发后，是否始终保持足够光滑，还是可能在有限时间内产生奇点。

这份候选证明选择构造反例：一个旋涡向内螺旋收缩，同时沿轴向不断拉长；局部速度增长至无界，但总能量维持有限，施加的外力仍然光滑。若全部条件均成立，它对应官方问题中的C和D两种反例选项，足以否定“所有允许条件下的解都永久保持光滑”这一命题。

这里的“速度无穷大”并不是对真实水流的日常预测，而是表示连续流体模型在有限时刻失去所要求的数学正则性。证明不能靠预先加入一个发散外力制造奇点；加速度、压力梯度、动量传递和黏性项必须以特定方式增长并精确抵消，才能让最终外力继续保持光滑。

Lean确认推导闭合，但不替人核对题意

Lean是一种证明助理。研究者把定义、假设、定理目标和推导步骤写成形式语言后，其内核会检查结论能否依据声明的前提与逻辑规则推出。通过检查意味着编码后的推导链条闭合，也大幅压缩了隐藏跳步、计算疏漏和前后不一致的空间。

但Lean验证的是代码里实际写下的命题，而不是新闻稿对结果的概括。外部专家仍要确认形式化目标是否与千禧年问题完全对应，初始状态、外力光滑性、能量、正则性和定义域等条件是否被忠实编码，以及分析论文的全部主张是否确实包含在机器检查的形式陈述中。

因此，“Lean接受了证明”与“数学共同体接受了解答”不是同一个结论。前者为形式系统内部的推导提供强证据；后者还要求未参与项目的偏微分方程专家读懂构造、复现检查，并排除证明借助定义差异回答了较弱问题的可能性。

四层证据不能相互替代

判断这项结果，需要区分四层证据：首先是作者公开论文并提出解题主张；其次是Lean内核接受指定的形式化陈述；第三是独立专家核对命题、假设和数学意义，并经过学术出版与同行评议；最后才是Clay数学研究所依照千禧年奖程序评估候选解答。

这四层回答不同问题。公开论文界定作者究竟主张了什么；机器检查判断编码后的结论能否由前提推出；独立审查检验形式化命题与原题的对应关系；正式程序则判断结果是否已获得足够广泛的数学认可。完成前两层，并不会自动完成后两层。

Clay现行千禧年奖规则 要求候选解答先在合格出版物发表，发表后至少经过两年，并获得全球数学界普遍接受，研究所才会考虑是否进入后续评估。由此可见，无论OpenAI是否申领奖金，正式认定都不可能在发布数日后完成。

88小时搜索之外，优先权争议仍未解决

OpenAI集中搜索的同时，纽约大学数学家Tristan Buckmaster和Levent Alpöge也在推进相关流体方程研究。他们以Diego Córdoba和Luis Martínez-Zoroa的工作为出发点，完成了与无黏性的Euler方程有关的结果；这与OpenAI所主张的受迫纳维—斯托克斯反例并非同一道命题，但研究路线、公开时间和方法来源出现交叉。

争议还涉及未公开草稿是否可能通过Codex影响竞争性研究，以及关于联合发布和署名安排的不同叙述。ABC News对双方公开说法的梳理 显示，Buckmaster表示无法判断其数据是否被使用，并明确没有直接指控任何人；他与OpenAI研究员Sébastien Bubeck对拟议署名方案的性质也给出了不同版本。

现有公开材料不足以把任何一方的叙述视为已经独立查明的事实。即使候选证明最终通过数学审查，谁提供了关键思路、谁先取得相关结果以及未公开数据是否受到妥善隔离，仍属于需要单独厘清的研究伦理与优先权问题。

当前结论仍是重大候选解答

截至2026年9月11日，可以确认的是：OpenAI已经公开一份针对纳维—斯托克斯千禧年问题反例选项的具体分析证明，并提供了通过机器规则检查的Lean形式化成果。它比单纯的公司声明或未经形式检查的自然语言草稿更接近可复核的数学结果，也足以被视为需要严肃审查的重大候选解答。

仍未确定的是，独立专家能否确认形式化目标、全部假设和核心构造与官方问题完全一致，以及论文能否经过出版、长期检验并获得数学界普遍认可。接下来真正能够改变结论的，是公开可复现的外部审查、对潜在缺口的回应和逐步形成的学术共识；在这些环节完成前，“已经解决”仍是OpenAI的主张，而不是正式定论。