OpenAI 的 Navier–Stokes 证明主张，一文读懂

Navier–Stokes 方程描述水和空气等流体如何运动。它们是流体动力学、工程和物理学的核心，但数学家至今还没有完全理解其在三维空间中的行为。

千禧年大奖难题版本大致问的是：光滑的初始条件是否总会在未来所有时间内产生光滑解，还是这些方程可能会“爆破”——产生一个奇点，使速度等某个量变为无穷大。克雷数学研究所在 2000 年将该问题列为七个千禧年大奖难题之一，每个难题对应 $1 million 奖金。在这次公告之前，七个问题中只有庞加莱猜想被解决，相关概述见维基百科。

据《Quanta Magazine》报道，OpenAI 的主张是：运行在内部模型上的自主 AI agent 在三维 Navier–Stokes 方程中找到了一个奇点。Quanta 报道称，这项工作使用了约 10,000 个 agent，这些 agent 在 88 小时后找到了一个证明，另一个 AI 模型又花了 17 小时将结果形式化到 Lean 中。这些 agent 交换了近 500 万条消息；据 Quanta 报道，OpenAI 的 Sébastien Bubeck 估算计算成本为数百万美元。

《MIT Technology Review》报道称，OpenAI 表示不打算申领这笔 $1 million 奖金。根据维基百科，该反例尚未经过外部数学家或克雷数学研究所验证。

最后这一点很重要。Lean 形式化是一个强信号，但它并不等同于学术共同体的接受。Quanta 指出，形式化证明可以证明某个命题在证明助手内部成立，而数学家仍需检查被形式化的命题是否在逻辑上等价于人们原本想证明的数学主张。

微分方程描述变化量之间的关系。在流体力学中，Navier–Stokes 方程结合了速度、压力、黏性、外力和质量守恒。用标准记号写下它们并不难，但理解它们的长期行为可能极其困难。

核心难点并不在于工程师能否模拟流体。他们一直在这样做。问题在于，在千禧年大奖难题规定的条件下，这些理想化的数学方程是否一定表现良好。

奇点意味着方程预测了某种崩溃：流体的某一部分会演化到一个不可能的数学状态。正如 Quanta 所解释的，这并不意味着现实工程中会立刻出现实际失效，因为真实流体由分子和原子构成，而不是完美光滑的连续体。但从数学上说，它将表明这些理想化方程的行为比许多人预期的更出人意料。

这个问题还与湍流有关，而湍流是物理学中最困难的现象之一。维基百科将湍流描述为物理学中最重大的未解问题之一，尽管它在科学和工程中非常重要。一个爆破解并不会在实际意义上“解决湍流”，但会重塑数学家对其背后方程的认识。

争议的焦点在于 OpenAI 的工作与 Buckmaster 和 Alpöge 的工作之间的关系。

Quanta 报道称，OpenAI 的公告发布在 Buckmaster 公布其与 Alpöge 在密切相关问题上的结果约 12 小时之后。他们的工作使用了多种 AI 模型，包括 OpenAI 模型。《MIT Technology Review》报道称，Buckmaster 和 Alpöge 已在这个问题上工作了将近一年，Buckmaster 发布了一份证明，表明 Navier–Stokes 方程的一个简化版本可能会崩溃。

OpenAI 的工作和 Buckmaster–Alpöge 的工作似乎都依赖一种与 Diego Córdoba 和 Luis Martínez-Zoroa 相关的方法。Quanta 称，两个团队都大量依赖 Córdoba 和 Martínez-Zoroa 的工作，后者提出了一种不同于大多数数学家所用方法的策略。《MIT Technology Review》引用 Brown University 数学教授 Javier Gómez-Serrano 的话称，这种方法是几个被认为对该问题有希望的方向之一。

据《MIT Technology Review》报道，OpenAI 已承认，其团队是在听到有关 Buckmaster 和 Alpöge 努力的传闻后，受到启发开始研究该问题的。争议在于 OpenAI 的模型或员工是否访问、训练于或以其他方式受益于 Buckmaster 和 Alpöge 的工作。

《MIT Technology Review》报道称，Buckmaster 发布了一份文件，描述了他与 OpenAI 员工的互动。根据 Buckmaster 的说法，OpenAI 员工提出了两种可能。Buckmaster 和 Alpöge 可以发布他们的工作，而 OpenAI 会在第二天发布其 Navier–Stokes 解；或者 Buckmaster 可以与 OpenAI 合作撰写一篇 Navier–Stokes 论文，但由于 Alpöge 与 Anthropic 的从属关系，将其排除在作者名单之外。《MIT Technology Review》还报道称，OpenAI 否认其员工或 agent 访问过 Buckmaster 和 Alpöge 的对话记录。

这些都是严重指控，但公开记录并不完整。正确的立场是将数学主张与署名归属争议分开。证明可以是正确的，而过程仍然在伦理上存在争议。或者证明可能在审查中失败，但署名归属问题仍然重要。

Lean 是一个证明助手：用于表达数学命题并检查每一步是否符合形式规则的系统。在高风险数学中，它可以消除很大一类错误。它也可以让 AI 生成的证明更容易审计，因为证明不只是散文式文字；它是可执行的形式逻辑。

这就是 Lean 组件重要的原因。如果形式化是可靠的，并且与目标 Navier–Stokes 命题相匹配，那么这个结果就更难被斥为流畅的幻觉。对 AI 构建者来说，这正是会写出看似合理推理的模型，与能生成可由另一个程序检查的产物的系统之间的区别。

但 Lean 并不能解决所有信任问题。它不能确立优先权。它不能揭示证明是如何被找到的。它不能说明私有数据、对话记录或未发表想法是否影响了搜索过程。它也不能取代数学共同体对证明意义进行解释的角色。

这种区别对于构建 AI 产品的人来说应该很熟悉。结构化输出、测试、评测和形式化检查可以让系统更可靠，但它们本身并不能回答治理问题。如果一个 AI agent 可以调用工具、检查日志、复用私有上下文，或与其他 agent 协作，那么系统需要边界和审计轨迹，就像需要原始能力一样。

这也是多 agent 工作是工程问题、而不只是 prompt 技巧的原因之一。无论你是在设计研究 agent 还是业务工作流，实际问题都很相似：哪些 agent 可以看到哪些上下文，它们可以调用哪些工具，交接在哪里发生，哪些内容会被记录？这些设计选择在风险达到千禧年大奖级别之前，就已经在 AI agent 中变得重要。

最引人注目的运营细节是规模。Quanta 报道称，约 10,000 个 agent、88 小时搜索、另外 17 小时形式化，以及近 500 万条 agent 间消息。《MIT Technology Review》报道称，OpenAI 表示这次运行耗资数百万美元。

这种规模并不是大多数学术团队能够获得的。它暗示了一种可能的未来：前沿数学进展取决于内部模型、私有算力预算，以及集中在少数 AI 公司内部的 agent 基础设施。

《MIT Technology Review》将其描述为数学的一个转折点：如果重大未解问题可以由私有 agent 集群发起攻击，学术协作规范可能会承受压力。数学家通常会从失败尝试、部分结果和错误转向中学习。如果这些过程发生在私有系统内部，且从未公开，这个领域或许会得到答案，却失去传统上催生新工具和子领域的共享路径。

Quanta 引用了 Princeton 数学家 Charles Fefferman 的话；他撰写了克雷研究所对该问题的官方描述，并表示自己对问题被解决感到兴奋，同时认为 Córdoba 和 Martínez-Zoroa 是这个故事中的英雄。这种归属判断是一个有益的校正。即使最后一步是自动化完成的，研究品味——选择一个有希望的方向——也来自人类多年积累的数学工作。

对构建者来说，教训不是“使用更多 agent”。而是 agentic 系统会放大它们所获得搜索空间的质量。更好的模型和更大的预算确实有帮助，但问题框定、上下文选择、工具访问和验证循环仍然决定系统是在探索有用区域，还是在燃烧算力。

如果你在多个模型之间路由工作，同样的原则也适用于更小规模的场景。为任务使用最合适的模型，但不要把模型选择当作整个系统。周围的工作流——检索、约束、检查、审批和日志——才是可靠性的来源。换句话说，能力来自整个工作流，而不是某个排行榜选择。

首先要关注的是数学验证。外部数学家和克雷数学研究所需要时间来评估该证明是否正确、Lean 形式化是否匹配目标主张，以及该结果如何纳入既有工作。

第二是署名归属。来自 OpenAI、Buckmaster、Alpöge 和外部数学家的公开说法尚未形成一份确定记录。核心问题是事实层面的：OpenAI 的 agent 或员工访问了什么，用什么进行了训练，知道了什么，以及何时知道。

第三是这是否会成为一种模板。如果前沿 AI 实验室可以把大规模 agent 集群指向著名未解问题，更多公告会接踵而至。有些会很干净。有些会存在争议。有些会在审查中失败。受影响的领域将需要围绕署名、披露、私有算力和 AI 辅助优先权主张建立规范。

对在纯数学之外构建 AI 的人来说，信息已经足够清楚：能力正在走向系统，而不是单个 prompt。Agent、工具、模型路由和验证正在成为工作的基本单元。能够妥善处理来源和审查的团队，会比只追求更大输出的团队处于更有利的位置。

随着验证与署名归属故事继续发展，我们会持续关注。如果你想获取保留技术上下文的 AI 新闻，可以订阅 LIA newsletter。

• OpenAI 声称，自主 AI agent 在三维 Navier–Stokes 方程中找到了一个奇点，并生成了 Lean 形式化证明。
• 该结果尚未被外部数学家验证，也尚未被克雷数学研究所接受。
• Lean 证明可以减少许多证明检查错误，但审查者仍需确认形式化命题与目标数学主张相匹配。
• 这次公告卷入了一场署名归属争议，涉及 Tristan Buckmaster、Levent Alpöge、Diego Córdoba 和 Luis Martínez-Zoroa 的工作。
• 据报道，这次运行的规模凸显了前沿 AI 实验室与大多数学术团队之间的资源差距。
• 对 AI 构建者来说，这一事件表明 agent 需要来源记录、审计轨迹、验证循环和清晰边界，而不只是更多算力。

本节回答 OpenAI Navier–Stokes 主张背后的实际问题：下面的回答涵盖公告内容、Lean 的作用，以及仍需独立审查的部分。它也将数学层面的利害关系与围绕该工作的署名归属争议区分开来。

OpenAI 表示它拥有一个 AI 生成的解答，但该主张仍需要外部数学审查，并需要克雷数学研究所评估。

根据所引用的报道，OpenAI 声称其 agent 在三维 Navier–Stokes 方程中找到了一个奇点，并且另一个模型将该结果形式化到 Lean 中。

Lean 可以检查每个形式化步骤是否符合规则，这让证明更难被视为看似合理的文字而被轻易否定。数学家仍需验证被形式化的命题是否匹配目标 Navier–Stokes 主张。

争议在于 OpenAI 的工作是否在没有适当署名的情况下，受益于 Tristan Buckmaster 和 Levent Alpöge 借助 AI 完成的研究。据《MIT Technology Review》报道，OpenAI 否认其员工或 agent 访问过他们的对话记录。

不能。爆破证明会重塑对流体运动背后方程的数学理解，但它不会直接把湍流作为一个实际工程问题来解决。