胜算云官网

OpenAI 宣布求解纳维-斯托克斯千禧年难题：88 小时智能体证明背后的优先权争议

精
精益前沿编辑部编辑于 2026-09-10
598 次阅读

9 月 8 日，OpenAI 官宣：其内部 AI 智能体系统给出了纳维-斯托克斯方程存在性与光滑性这一千禧年大奖难题的解答——证明初始光滑的三维流体可在有限时间内形成奇点（blow up），并附上证明文稿与 Lean 形式化验证。这本该是 AI for Math 的历史性时刻，但不到 24 小时，纽约大学数学教授 Tristan Buckmaster 与任职于 Anthropic 的数学家 Levent Alpöge 公开指控 OpenAI 不正当竞争，一场围绕优先权、署名与「AI 实验室能否被信任」的争论迅速发酵。

流体涡旋与奇点意象图
三维流体的旋转涡流在数学模拟中碎裂为粒子——本次证明的核心，正是光滑流体会不会在有限时间内「崩溃」成奇点。

事件背景：约 90 年未解的流体方程

纳维-斯托克斯存在性与光滑性问题问的是一个看似简单的问题：三维不可压缩流体的运动，从光滑的初始条件出发，其解是否永远光滑、可控？还是会在有限时间内「崩溃」，形成速度无穷大的奇点？这是克雷数学研究所 2000 年悬赏百万美元的七大千禧年难题之一，自方程提出以来已悬置约 90 年，是流体力学与偏微分方程理论的圣杯。

在 OpenAI 宣布之前，学界主流进展仍停留在构造特殊方程的 blowup 反例上——而这正是 Buckmaster 与 Alpöge 的主攻方向：9 月 8 日早些时候，两人刚刚公布了针对带光滑强迫的不可压缩多孔介质方程的三项有限时间 blowup 结果。

机制：88 小时智能体求解，3000 亿 token，Lean 验证 17 小时

根据 OpenAI 的公告与各方披露，这次求解的组织方式前所未有：

  • 模型：由一组智能体驱动一个尚未发布的下一代模型，能力显著超过 GPT-6 Astra；
  • 节奏：研究始于 9 月 1 日，约 88 小时内完成求解，总计消耗约 3000 亿个输出 token——按 Astra 的 API 价格估算约 2250 万美元；
  • 结论：给出 Navier-Stokes 方程的一个 blow up 解，即证明初始光滑的流体可在有限时间内形成奇点，并附完整证明文稿；
  • 验证：经 GPT-6 Astra 用约 17 小时完成 Lean 形式化验证，机器可检验的证明是这次发布最硬的底气。

OpenAI 研究科学家 Noam Brown 承认这次证明「花费了数百万美元」，但认为成本会快速下降。Emad Mostaque 则直接称这是「迈向 ASI 的里程碑事件」。

各方回应：从优先权之争到开放科学之问

争议在官宣当天爆发。Buckmaster 与 Alpöge 称，两人的研究进展信息被泄露给 OpenAI，对方随后用大量算力沿其独特路线追赶证明——两人此前曾使用 Codex 和 Claude 在该问题上取得初步进展。OpenAI 的 Bubeck 否认了不正当竞争的指控。

Sam Altman 随后发回应：对方手中只有 Euler 方程的结果，双方围绕联合发布的协调失败，并称对方曾以抄袭指控相威胁。

9 月 9 日，Buckmaster 通过公开声明把指控升级：OpenAI 曾向他施压、拒绝给他的合作者 Alpöge（因任职 Anthropic）署名，且可能用两人上传到 Codex 的研究草稿训练模型——他称这是「绝对的学术不端」。The Decoder 评论称，这场争议真正提出的问题是：研究者还能信任 AI 实验室吗？

学界的冷静声音同样值得关注。Hugging Face 联创 Thomas Wolf 认为「AI 数学尚未被解决」，OpenAI 的结果「更像是反例搜索，而非完整证明」；Simon Willison 则在梳理事件时肯定了「88 小时求解 + 17 小时 Lean 验证」的工程意义，同时提醒形式化验证才是这类声明可信度的关键。

时间线要点

  • 9 月 1 日：OpenAI 智能体团队启动该问题的研究（约 88 小时、3000 亿输出 token）。
  • 9 月 8 日早间：Buckmaster 与 Alpöge 公布三项有限时间 blowup 结果（带光滑强迫的不可压缩多孔介质方程），并公开与 OpenAI 的沟通经过。
  • 9 月 8 日 10:00：OpenAI 官宣内部 AI 系统给出 Navier-Stokes 解答，附证明文稿与 Lean 形式化验证。
  • 9 月 8 日晚间：Sam Altman 回应争议；Noam Brown 谈成本；Bubeck 否认不正当竞争指控。
  • 9 月 9 日：Buckmaster 指控升级（施压、拒署名、疑似用 Codex 草稿训练）；Thomas Wolf、Simon Willison 等发声，争论转向开放科学与信任问题。

编辑部的看法

单看技术，这是一次震撼的演示：反例搜索 + 大规模算力 + Lean 形式化验证的组合拳，把「AI 做数学」从新闻稿变成了机器可检验的工件。但争议暴露的短板同样真实——当实验室 unpublished 模型的成果与外部数学家的工作犬牙交错时，署名规则、草稿数据的使用边界、发布协调的伦理，都还停留在行业惯例而非制度约束。AI for Math 的下一个瓶颈可能不是算力，而是信任架构。

数据来源与原文出处

数据来源：AIHOT（热点聚合时间线）

—— 完 ——