OpenAI称内部AI系统生成并形式化验证纳维–斯托克斯方程解：数学界尚待独立复核

OpenAI 宣布其内部多智能体系统生成并用 Lean 形式化验证了一个关于三维不可压缩纳维–斯托克斯方程的奇点构造，主张对应克雷千禧年问题的 C、D 情形，但该结果尚需外部数学界独立复核与审查。发布同时引发研究优先权争议，并指出形式化验证并不能替代对定义与物理含义的人工审查。

OpenAI 9月8日宣布，其一个尚未公开的内部人工智能系统生成了一份关于三维不可压缩纳维–斯托克斯方程的分析证明，并同步发布了论文说明和 Lean 形式化版本。公司称，这一结果证明带有光滑外力的流体可以在有限时间内形成速度无界的奇点，对应克雷数学研究所千禧年大奖问题中的 C、D 两种情形。

但这并不等于数学界已经确认纳维–斯托克斯问题被解决。OpenAI公开的是自己的证明主张和形式化材料，外部数学家仍需检查其数学含义、假设和论证是否准确；克雷数学研究所也尚未宣布接受这一结果。OpenAI同时表示，不打算据此申请100万美元的千禧年大奖。

OpenAI公布了什么

纳维–斯托克斯方程用于描述流体运动，相关模型被用于飞机设计、天气预报和血液流动研究。问题的核心在于：对于三维不可压缩、具有黏性的流体，如果初始状态足够光滑，速度是否始终保持光滑，还是可能在有限时间内变得无界，形成所谓奇点。

OpenAI在官方说明中称，其系统构造了一个从静止状态开始的流动：在任意正黏性条件下，速度会在有限时间内变得无界，但动能保持有界，外部施加的力仍然是光滑的，并且具有紧支集。该公司将这一构造解释为一个不断向内螺旋、变得越来越细长的涡旋，流体核心收缩并加速，最终在有限时间内发生速度发散。

OpenAI发布的论文称，所构造的流动满足纳维–斯托克斯方程，并对应克雷问题陈述中的 C 情形。由于构造具有紧支性质，论文进一步给出周期环面上的对应结果，即 D 情形。

克雷数学研究所的官方问题说明把问题分成四种可接受的结果：A、B要求证明在整个三维空间或周期空间中解始终存在且光滑；C、D则要求构造一个光滑初始条件和光滑外力，使得不存在满足相应光滑性与能量条件的全局解。OpenAI此次主张的是后两种“失效”情形，而不是证明所有三维流动都会发生奇点。

一万名智能体协作，17小时完成 Lean 核验

OpenAI表示，这项工作始于9月1日。公司在8月底开始训练一个新的内部模型，随后因听到“两个千禧年大奖问题可能已经被解决”的传闻，决定让多智能体系统尝试多个开放数学问题。

其中，纳维–斯托克斯小组约有1万名并发智能体。智能体可以读取缓存互联网内容、运行代码，并在不同小组内交换信息。OpenAI称，这些智能体在9月5日、项目启动约88小时后得到结果；随后由 GPT-6 Astra 用约17小时把论证形式化并在 Lean 中验证。

公司给出的纳维–斯托克斯项目统计包括约270万条智能体消息和约1300亿个输出 token。所有尝试的问题合计约产生490万条消息、使用约3000亿个输出 token。英国广播公司援引 OpenAI 的价格估算称，仅纳维–斯托克斯这一轮工作的计算成本可能达到约1000万美元；Axios则报道称，OpenAI研究人员在记者电话会上将整体成本描述为“数百万美元”级别。不同估算取决于所采用的模型价格和计算口径，因此不应视为审计后的项目成本。

OpenAI还公开了NavierStokesAndEuler GitHub仓库。仓库包含纳维–斯托克斯和欧拉方程相关 Lean 4 形式化代码，并说明可以使用 Lean 4.34.0-rc2、Mathlib 和 Lake 构建。仓库称，形式化覆盖实数空间和周期环面两种结果，并对应克雷问题中的 C、D 情形。

Lean 的作用是检查形式化代码是否符合指定逻辑系统中的规则。它可以提高论证的机械可检查性，但不能单独回答一个更基础的问题：代码中的定义是否准确表达了论文中的数学对象，定理名称和物理解释是否与实际证明内容一致。外部数学家仍需把形式化结果与原始方程、边界条件和问题陈述逐一对照。

这与“证明了湍流”并不是一回事

纳维–斯托克斯方程与湍流研究密切相关，但 OpenAI的结果不应被简化为“AI已经解释了湍流”。公司主张的具体内容，是在一个特定构造中证明有限时间奇点可以出现；这回答的是方程解的存在性与光滑性问题中的一种允许情形。

它也不意味着现实中的每一种流体都会在有限时间内速度无限增大。论文讨论的是满足特定条件的数学构造，而不是对飞机周围气流、河流或人体血流的普遍预测。现实流体还涉及分子尺度、边界、可压缩性和其他超出理想化方程的问题。

从问题本身看，克雷的 A、B 情形关注无外力情况下任意合适初始数据的全局光滑性；C、D则允许构造特定的外力和初始条件来展示全局光滑解不存在。OpenAI的结果若最终被接受，意味着后两种情形得到解决，并不等同于所有关于纳维–斯托克斯方程的分析问题都已结束。

结果公布之际出现了优先权争议

OpenAI的发布也伴随着一场关于研究来源和优先权的争议。英国广播公司和Axios报道，纽约大学数学家 Tristan Buckmaster 与 Anthropic研究员 Levent Alpöge此前也在研究相关流体动力学问题。Buckmaster在公开声明中表示，他在9月3日获悉有关其团队研究进展的信息已经传达给 OpenAI，并对 OpenAI何时开始研究该问题、以及相关信息是否可能影响其工作提出疑问。

OpenAI则表示，研究人员和智能体在相关团队公开发布工作之前，没有通过任何方式看到两人的研究；公司还说，没有人为解决纳维–斯托克斯问题而搜索用户数据。不过，OpenAI同时承认，无法完全排除从产品使用中产生的去标识化数据曾改善模型的可能性，并强调两边的证明和具体结果存在明显差异。

这些说法目前代表争议双方的陈述，不等同于已经完成的独立调查结论。对于 AI 参与科学研究而言，争议的重点不仅是证明是否成立，也包括模型训练数据、研究工具权限、未公开研究成果的保密边界，以及实验记录能否被外部复现。

这也是为什么，OpenAI此次发布应被理解为一项需要审查的研究主张，而不是已经获得数学界认证的最终定论。英国广播公司的报道指出，克雷数学研究所尚未独立验证或公开接受这一结果；Axios的报道则把重点放在证明主张与外部研究优先权争议的交叉处。

AI数学研究的瓶颈可能从“生成”转向“验证”

OpenAI此次项目展示了多智能体系统在长周期数学任务中的一种工作方式：不同小组并行尝试多个方向，通过共享中间结果和代码反馈缩小搜索范围，再由另一个模型负责形式化和核验。此前，Anthropic也曾公布Claude代理团队完成费马大定理 Lean 形式化，但该项目的重点是把人类已经证明的定理转化为机器可检查代码，而不是独立发现新的数学结论。

OpenAI这次的说法更进一步：公司声称智能体不仅完成了形式化，还生成了一个此前未被数学界接受的奇点构造。如果这一主张经得起审查，其意义将不只是模型能够写出大量证明代码，还包括模型能否在复杂偏微分方程中提出可行的结构、处理多个尺度之间的相互作用，并把这些构造压缩为人类数学家可以审阅的论证。

不过，计算规模也说明了这种方法的现实代价。约1万名并发智能体、数百万条消息和数千亿个输出 token，意味着“88小时完成”不能简单理解为一个模型独自思考了88小时。它更接近一项高成本的并行研究工程：模型能力、任务编排、代码执行、状态管理和人类筛选共同构成结果。

在类似的科学工作流中，AI代理可以增加候选方案和实验步骤的吞吐量，但最终的科学责任仍集中在人类研究者身上。OpenAI近期关于代理参与真实实验的案例也显示，模型可以承担受控的测量和分析任务，却仍需要研究人员处理含糊信号、异常结果和最终判断。[AIFlux此前对 GPT‑5.6 Sol参与量子实验校准的报道](https://aifluxnews.com/gpt-5-6-sol-%E5%A6%82%E4%BD%95%E5%B8%AE%E5%8A%A9%E8%BF%90%E8%A1%8C%E9%87%8F%E5%AD%90%E8%AE%A1%E7%AE%97%E5%AE%9E%E9%AA%8C%EF%BC%9A%E4%BB%8E%E8%87%AA%E5%8A%A8%E6%A0%A1%E5%87%86%E5%88%B0%E4%BA%BA/】也提出了类似边界：自动化可以延长和加速流程，但不能自动替代对结果的解释与承担责任。

仍待回答的问题

接下来最关键的不是 OpenAI是否使用了足够多的智能体，而是外部专家能否确认以下几点：

• 论文中的速度发散、有限动能和光滑外力是否在同一构造中同时成立；
• 从局部剖面、渐近展开到全局拼接的每一步是否满足三维纳维–斯托克斯方程；
• Lean代码是否完整覆盖论文宣称的关键数学步骤，而不只是验证了较低层次的形式化片段；
• C、D两种情形与克雷数学研究所官方问题的假设是否逐项一致；
• 证明是否能够由独立研究者在公开工具链中复现并理解；
• OpenAI与 Buckmaster、Alpöge之间关于研究信息流动和优先权的争议，是否会出现更多可核查材料。

在这些问题得到回答前，最准确的表述是：OpenAI公布了一项由内部 AI 系统生成、并配有 Lean 形式化材料的纳维–斯托克斯奇点构造，并主张它对应千禧年问题的 C、D 情形。它可能成为 AI辅助数学研究的重要案例，但是否构成数学界认可的千禧年问题解答，仍需独立复核。

来源： OpenAI官方说明；OpenAI论文《Finite time blowup for Navier–Stokes》；OpenAI NavierStokesAndEuler Lean仓库；克雷数学研究所官方问题说明；BBC报道；Axios报道。