OpenAI 说：他们内部一套智能体（能自己多步干活、还能上网查资料跑代码的 AI）给出了纳维–斯托克斯千禧年问题的解。
用的不是已经推给大家的 GPT-6 Astra，而是「明显更强、还在继续训练」的下一代内部模型。证明写出来了，还用 Lean 做了形式化。
一句话：不是又刷榜，是直接碰数学界最硬的那一类题。
链接
官网长文：https://openai.com/index/navier-stokes-solution/
官方发帖：https://x.com/OpenAI/status/2097374640582668336
OpenAI 官方发帖配图
官网页面配图
这个问题是啥
纳维–斯托克斯方程，是用来描述流体怎么动的：飞机周围的气流、天气预报里的风、血管里的血流，很多工程模型都会碰到它。
方程把流体当成连续介质，而不是一个个分子。麻烦在于：如果一开始流动很光滑，后面会不会在有限时间里「崩掉」——速度变得无限大，出现数学上的奇点？
真流体不可能跑出无限速度。所以如果方程允许奇点，就说明这套连续介质近似在那里失效了，得换更细的描述。
这道题纠缠了大约九十年。2000 年，克雷数学研究所把它列为七大千禧年问题之一，悬赏百万美元。
克雷研究所题面：https://www.claymath.org/millennium-problems/navier-stokes-equation/
他们说证了啥
官方写法是：系统给出了解析证明，并用 Lean 形式化——起初光滑、静止的流体，在有限外力作用下，可以在有限时间里长出奇点；过程中能量仍然有限。
这对应官方千禧年题面里的 C（以及 D）陈述：不是「永远光滑」，而是「可以爆破」。
画面感上，他们形容解是一个涡：流体打着旋往里收，中心越来越细长，像意大利面一样被拉长；中心缩小、转速变快，但能量还卡在有限范围里。难的是：奇点要靠流体自己的运动长出来，不是人手塞一个无限外力。
官网示意图：局部不可压缩流动（橙快青慢）
怎么找出来的
• 8 月 28 日起在训新的内部模型，数学等基准上出现「台阶式」提升，训练还在继续。
• 9 月 1 日听到「有千禧年问题被解决」的传闻，于是拿这套系统去试所有未解千禧年题，外加几道高影响力题。
• 智能体分小组协作，能读缓存过的网页、能跑代码；解出纳维–斯托克斯的那组大约有一万个并发智能体。
• 先意外解决了去掉黏性项的欧拉方程正则性问题（无外力版本），大约一百个智能体干了约五十小时；随后把资源压到纳维–斯托克斯上。
• 9 月 5 日左右给出解析解，距启动约八十八小时；再用 GPT-6 Astra 做 Lean 形式化与核验，大约十七小时。
• 整场尝试：大约四百九十万条消息、三千亿输出 token；其中纳维–斯托克斯这条线大约二百七十万条消息、一千三百亿输出 token。
官方串推：约一万智能体、八十八小时
同期还有谁
OpenAI 写得很直：他们 9 月 1 日听到的传闻，后来发现和 Anthropic 员工 Levent Alpöge、纽约大学数学教授 Tristan Buckmaster 的工作有关。
对方公开的是带外力的欧拉爆破；OpenAI 这边欧拉是无外力版本，纳维–斯托克斯是完整黏性方程上的奇点。官方说证明路线差很多，并承认对方在强制欧拉上的优先权。
他们另发一条澄清：研究人员和智能体在对方公开发表前没有看到其工作；没有为了解题去读具体用户数据。同时加了一句：虽不太可能，但不能排除「去标识化后的产品使用数据」曾帮模型变强。
澄清帖：https://x.com/OpenAI/status/2097375276384567642
火了吗
官方主帖截至本稿：大约两千一百万展示、近七万赞、一万一千多转发、八千多引用、三千多回复、一万七千多收藏——量级已经是「全网都在看」那一档。
纽约时报、科学美国人等也都跟了。数学圈的态度会更硬：证明和 Lean 形式化已经放出来，但真正落地还要靠同行逐页拆。
奖金呢
OpenAI 明确说：这次发布是为了汇报模型进展，不打算用这个结果去申领千禧年奖金。
他们更想强调的另一句是：这只是能力跃进的一张快照，接下来会把精力放在理解这套更强模型，并考虑怎么更克制地推进。
官网原文（全文中英对照）
以下按 OpenAI 官网长文顺序，英文原句 + 中文意译。
原文：https://openai.com/index/navier-stokes-solution/
On the Navier–Stokes Millennium Prize Problem
（意译）关于纳维–斯托克斯千禧年问题
We’re sharing a solution to the Navier–Stokes existence and smoothness problem, one of the Millennium Prize Problems. This proof, produced by an internal OpenAI system, shows that the dynamics of the Navier-Stokes equations for fluid motion can develop a singularity in finite time. We’re sharing both a writeup of the proof and a formalization in Lean.
（意译）我们公布纳维–斯托克斯「存在与光滑性」问题（千禧年问题之一）的一个解。这份由 OpenAI 内部系统给出的证明表明：描述流体运动的纳维–斯托克斯动力学，可以在有限时间里长出奇点。我们同时公开证明文稿，以及 Lean 形式化。
The Millennium Prize Problems represent some of the deepest questions at the frontier of mathematics. The question of whether smooth three-dimensional fluid motion can break down has remained unresolved for roughly 90 years.
（意译）千禧年问题代表了数学前沿里最深的一类问题。三维光滑流体运动会不会「崩掉」，大约纠缠了九十年。
A major goal of our work is to empower scientists to advance research and technology that benefits all of humanity. To solve the Navier–Stokes problem, we used an internal model that is significantly more capable than GPT‑6 Astra. We believe it is important to inform the world about the pace of AI progress and what to expect from upcoming models.
（意译）我们工作的一大目标，是让科学家能推进造福全人类的科研与技术。为了解这道题，我们用了明显强于 GPT-6 Astra 的内部模型。我们认为有必要让外界知道 AI 进展的速度，以及接下来的模型大概会是什么水准。
The problem / 问题本身
The Navier–Stokes equations use Newton’s second law of motion (“F=ma”) to describe how fluids move. Importantly, they treat a fluid as a continuous medium rather than tracking individual molecules. These equations are used for aircraft design, weather forecasting, and the study of blood flow.
（意译）纳维–斯托克斯方程用牛顿第二定律（F=ma）描述流体怎么动。关键是：它把流体当成连续介质，而不是一个个分子来追。飞机设计、天气预报、血流研究都会用到它。
A fundamental open question for these dynamical equations has been whether the continuum approximation of the fluid can break down. Specifically, can the Navier–Stokes equations for a three-dimensional incompressible fluid with constant density develop a “singularity,” even when the motion starts smoothly? Here, a singularity means the dynamics lead to speeds in the fluid growing without bound within a finite amount of time. The development of a singularity would have to happen despite the presence of viscosity, which tends to smooth out motion. Because a real fluid cannot move infinitely fast, this would mark a breakdown in how the equations model the fluid. To continue modeling the system, one would then need to track the behaviour of each particle individually.
（意译）这些动力学方程有一个根本未解问题：连续介质近似会不会失效？具体说，三维、常密度、不可压缩流体的纳维–斯托克斯方程，即便一开始运动很光滑，会不会长出「奇点」？这里的奇点是指：在有限时间里，流体速度变得无限大。黏性本来会把运动抹平，奇点却要在黏性还在时长出来。真流体不可能无限快，所以一旦出现奇点，就说明这套方程对流体的建模在那里崩了；要继续建模，就得改成一个个粒子去追。
The equations date to the nineteenth-century work of Claude-Louis Navier and George Gabriel Stokes. In 1934, Jean Leray proved that solutions exist in a generalized sense, but whether they always remain smooth became a central unanswered question. In 2000, the Clay Mathematics Institute named the Navier–Stokes existence and smoothness problem one of seven Millennium Prize Problems.
（意译）方程可追溯到十九世纪 Navier 与 Stokes 的工作。1934 年，Leray 证明了广义意义下解存在，但解是否永远光滑，成了核心悬题。2000 年，克雷数学研究所把纳维–斯托克斯存在与光滑性，列为七大千禧年问题之一。
The result / 结果
Our system produced an analytical proof and a Lean formalization that an initially smooth fluid at rest can develop a singularity in a finite time. The fluid has a smooth force applied to it, and its energy remains finite through the entire dynamics, from rest to the formation of the singularity. This resolves the Navier–Stokes Millennium Prize problem by establishing statement “C” (and also “D”) in the official Millennium Prize formulation.
（意译）我们的系统给出了解析证明和 Lean 形式化：起初光滑、静止的流体，可以在有限时间里长出奇点。流体上作用着光滑外力，从静止到奇点形成，能量始终有限。这对应官方千禧年题面里的陈述 C（以及 D），从而解决了这道千禧年问题。
The solution is a vortex, a spinning swirl of fluid, that spirals inward and gets increasingly elongated, like spaghetti. This central region shrinks while it speeds up in such a way that its energy still stays finite, as required by the laws of physics. The technical challenge is for the equations to develop the breakdown through the motion of the fluid itself, rather than, for example, us putting in an infinite force by hand. More mathematically, the terms in the Navier–Stokes equations that describe the motion—acceleration, pressure gradients, momentum transfer, viscosity—must both become big yet cancel in a precise way. This detailed balance leaves a smooth external force even as the velocity of the fluid grows without bound.
（意译）解是一个涡：流体打着旋往里收，中心越来越细长，像意大利面。中心一边缩小一边加速，能量仍保持有限，符合物理要求。技术难点在于：崩塌要靠流体自己的运动长出来，而不是人手塞一个无限外力。更数学地说，描述运动的各项——加速度、压力梯度、动量传递、黏性——既要一起变大，又要精确对消；这种细致平衡下，外力仍光滑，流体速度却可以无限变大。
A snapshot of local incompressible motion. Orange marks faster angular rotation; teal marks slower rotation. Circulating speed also depends on radius. The trajectories show inward spiraling and axial stretching.
（意译）（图注）局部不可压缩运动的一帧。橙色表示角速度更快，青色更慢；环流速度也随半径变化。轨迹显示向内螺旋与轴向拉伸。
How we found the proof / 证明是怎么找到的
Since August 28 we have been training a new internal model that has exhibited unprecedented performance in our benchmarks, including mathematics. This model’s training is ongoing and its performance continues to improve.
（意译）自 8 月 28 日起，我们在训练一个新的内部模型，它在包括数学在内的基准上表现出前所未见的水平。训练仍在继续，表现还在涨。
On Tuesday, September 1, we heard rumors that two Millennium Prize problems had been resolved. Inspired by these rumors and by the step change in performance of our internal model, we launched an effort to evaluate it on all open Millennium Prize problems and a few other high-impact problems.
（意译）9 月 1 日（周二），我们听到传闻：有两道千禧年问题已被解决。受传闻和内部模型台阶式提升鼓舞，我们启动评估：拿它试所有未解千禧年题，外加几道高影响力题。
We used a system of coordinating agents powered by our internal model. The agents had access to tools such as the ability to read from a cached version of the internet and the ability to run code. Agents were subdivided into groups with the ability to communicate within the group. The groups varied in size, and the group that produced the Navier–Stokes resolution involved on the order of 10,000 concurrent agents. At all times we maintained the same strict safeguards that we apply to all our frontier model evaluations, including monitoring and isolation.
（意译）我们用的是由该内部模型驱动的协作智能体系统。智能体能读缓存过的互联网、能跑代码；再分成可组内通信的小组。小组规模不一，解出纳维–斯托克斯的那组大约有一万个并发智能体。全程沿用前沿模型评估的严格安全措施，包括监控与隔离。
For each problem, we prompted different groups of agents with different variants of the problem statement, covering all variants of the problem. For the Navier–Stokes problem, we suggested versions “A” and “B” (particular forms of the Navier–Stokes problem which would result in a proof) and versions “C” and “D” (which would result in a disproof) to separate groups of agents.
（意译）对每道题，不同小组拿到不同题面变体，覆盖全部变体。对纳维–斯托克斯，我们把 A、B（会导向「证明」的特定形式）和 C、D（会导向「反证 / 爆破」）分给不同小组。
In addition to the full Millennium Prize problems, we asked our multiagent system to try a set of “easier” problems. One of these problems was a similar blowup question for the limit of the Navier–Stokes problem with the viscosity term removed. This is known as the regularity problem for the Euler equations, and our agents surprised us by resolving this question. The specific variant of the question that they resolved was the unforced version, where no external force is applied to the fluid. Nearly 100 agents worked together for approximately 50 hours to produce our Euler regularity disproof.
（意译）除了完整千禧年题，我们也让多智能体系统试一组「更容易」的题。其中一道是去掉黏性项后的类似爆破问题，即欧拉方程正则性。智能体居然解了出来：具体是无外力版本。大约一百个智能体协作约五十小时，给出了我们的欧拉正则性反证。
Once we saw the Euler solution, we thought that Navier–Stokes was the most promising problem to work on. Thus, we decided to devote our resources to Navier–Stokes. To do so, we shifted agents away from the other Millennium Problems and prompted these agents with the Euler resolution. When a further trained version of our internal model became available over the course of the effort, we updated our agents to that model.
（意译）看到欧拉结果后，我们觉得纳维–斯托克斯最有希望，于是把资源压过去：从其他千禧年题抽调智能体，并把欧拉解喂给它们。过程中内部模型又训出更强版本，就同步升级智能体所用模型。
We encouraged different groups of agents to explore a diversity of approaches. After some time, we cross-pollinated the agent groups by using Codex to consolidate the most useful insights from each agent group. These follow-up prompts drew on the agents’ own intermediate results. The group that found the solution to Navier–Stokes was guided in such a way.
（意译）我们鼓励各小组走不同路线。过一段时间后，用 Codex 汇总各组最有用的洞见，做交叉授粉；后续提示词建立在智能体自己的中间结果上。最终解出纳维–斯托克斯的那组，就是这样带出来的。
The agents arrived at their resolution on Saturday, September 5, about 88 hours after the first agents were launched. Lean formalization and verification took an additional 17 hours via GPT‑6 Astra.
（意译）智能体在 9 月 5 日（周六）给出解析解，距第一批启动约八十八小时。Lean 形式化与核验再用 GPT-6 Astra，额外大约十七小时。
Across all attempted problems, the agents sent 4.9 million messages and used about 300 billion output tokens. In the process of resolving the Navier–Stokes problem, the agents sent 2.7 million messages and used approximately 130 billion output tokens.
（意译）所有尝试过的题合计：智能体发了约四百九十万条消息，用掉约三千亿输出 token。其中纳维–斯托克斯这条线：约二百七十万条消息、约一千三百亿输出 token。
Concurrent work / 同期工作
Our effort began on September 1st after hearing a rumor which we later realized was related to Levent Alpöge, an Anthropic employee, and Tristan Buckmaster, a math professor at NYU. After the completion of our full project and Lean verification (on September 6th), believing from the rumor they also had a solution of Navier–Stokes, we reached out to them to offer a concurrent release of our result and to recognize their priority in a joint announcement. At that point we found out that they had a resolution of the forced Euler problem. In these discussions we offered them visibility into all of the prompts we used and later to see the proof. We recognize the priority of their work on forced Euler and congratulate them on their remarkable mathematical achievement.
（意译）我们的行动始于 9 月 1 日听到的传闻，后来发现与 Anthropic 员工 Levent Alpöge、纽约大学数学教授 Tristan Buckmaster 有关。完整项目与 Lean 核验在 9 月 6 日完成后，我们以为对方也有纳维–斯托克斯的解，于是联系他们，提议同步发布并在联合公告中承认其优先权。此时才得知对方解的是带外力的欧拉问题。讨论中我们向他们展示了全部提示词，并随后让他们看证明。我们承认其在强制欧拉上的优先权，并祝贺这一出色的数学成就。
We (the researchers and the agents) did not see any of their work through any means until they released it publicly — in particular, no specific user data was accessed in order to solve this problem. While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models. However, our proofs differ significantly and even the precise results proved are different in the Euler case (forced vs unforced).
（意译）我们（研究人员与智能体）在对方公开发表前，没有通过任何途径看到其工作——尤其是，没有为了解题去访问具体用户数据。虽不太可能，但不能排除「由其产品使用衍生的去标识化数据」曾帮助模型变强。不过两边证明差异很大，欧拉情形下精确结果也不同（有外力 vs 无外力）。
Progress and responsibility / 进展与责任
Our goal in releasing this result is to report on the substantial progress of our AI models. We do not intend to claim the Millennium Prize for this result.
（意译）发布这一结果，是为了汇报 AI 模型的实质进展。我们不打算为这个结果申领千禧年奖金。
This milestone represents substantial work by mathematicians and AI researchers. However, this is not a culmination, but rather a snapshot in time, of progress on AI development.
（意译）这一里程碑凝聚了数学家与 AI 研究者的大量工作。但它不是终点，只是 AI 发展进程中的一张快照。
We believe we are now in the next period of AI progress, and today’s results provide further evidence of this. We are focusing on understanding this model, and using what we learn to help us guide and pace how we pursue further advances in capability. One of our key goals is to build AI systems which are steerable, accountable, and connected to people, which may require more deliberate choices about the pace of progress, as we continue our mission to ensure AGI benefits all of humanity.
（意译）我们相信 AI 已进入下一阶段，今天的结果是又一份证据。我们正专注理解这套模型，并把学到的东西用来引导、把控后续能力推进的节奏。关键目标之一，是做出可驾驭、可问责、与人相连的 AI；这可能要求对进展速度做更审慎的选择——我们仍在履行「让 AGI 造福全人类」的使命。
Author: OpenAI
（意译）作者：OpenAI
全文对照依据 OpenAI 官网；意译仅供阅读，以英文原文为准。
