当AI证明数学，学界的规则不够用了——OpenAI、Navier-Stokes与一场优先权之战

2026年9月8日，OpenAI宣布：一个内部AI系统已经证明，Navier-Stokes方程可以在有限时间内发展出奇点。这是7个克雷千禧年大奖难题之一，价值100万美元，90年来困扰着全球最顶尖的数学家。

消息发出后的24小时，数学界爆发了一场公开的争议——不是关于证明的正确性，而是关于谁发现了它，以及AI时代的科研规则是否还管用。

Navier-Stokes方程是流体力学的基石。19世纪由Claude-Louis Navier和George Stokes建立，它用牛顿第二定律描述流体（水、空气、血液）如何运动。飞机设计、天气预报、心血管医学——都依赖这组方程。

这组方程有一个未解之谜：当流体运动从一个完全光滑的状态出发，它是否可能在有限时间内发展出”奇点”——即某处流速趋向无穷大？如果会，意味着方程在某些物理条件下失效，需要重新构建描述框架。

这个问题从1934年Jean Leray提出广义解理论后，数学家们花了90年没能回答。

OpenAI的AI系统给出的答案是：会。存在一类满足初始条件的三维不可压缩流体解，其速度会在有限时间内趋向无穷大。证明已用Lean编程语言完成形式化验证。

OpenAI研究部门负责人Mark Chen说，这个证明的算力成本”高达数百万美元”——这也是这家公司在同一天顺带披露的信号：他们正在向外界暗示，驱动这个证明的内部模型，比GPT-6 Astra更强大得多。

1万个AI智能体，88小时：数学史上最昂贵的协作

OpenAI数学家Sebastien Bubeck在发布会上描述了关键细节：

8月28日，OpenAI开始训练一个具备高级数学能力的全新内部模型。随后，团队获悉Anthropic方向有进展——具体来说，纽约大学数学家Tristan Buckmaster和Anthropic研究员Levent Alpöge，可能在Navier-Stokes的核心子问题”非受迫欧拉方程”上取得了突破。

OpenAI随即加大资源投入。超过1000个AI智能体开始并行攻克这个问题；在关键阶段，同时运行的智能体一度多达10,000个。50小时后，证明的雏形出现。88小时后，Lean形式化证明完成。

“我认为肯定哪里出错了，”Bubeck说。”但周日早上我们得到了最终解，Lean形式化，一切都完整。”

就在当天，Buckmaster和Alpöge在Mastodon上发布了他们关于非受迫欧拉方程的关键进展。他们也使用了AI工具——Claude和Codex——但作为数学家主导的辅助手段。

然后，故事开始变得复杂。

署名之战：三条指控，一张截然不同的图景

Buckmaster随后发布了一份正式声明，描述了他眼中的事件经过。

指控一：OpenAI在得知他们工作后加速冲刺

上周，Buckmaster得知OpenAI已经获悉了他和Alpöge的研究方向，并随即大规模投入算力攻克这个问题。这在人类数学家之间，通常被视为”赶发”（scooping）——一种学界公认的不道德行为。

指控二：训练数据问题无法厘清

Buckmaster询问OpenAI，是否查看了他们的Codex使用日志。得到的回复是”模型没有查看用户数据”，但对”训练数据”的追问，没有明确答复。OpenAI官方声明写道：”虽然不太可能，但我们无法排除来自他们使用我们产品的去标识化数据帮助改进了我们的模型。”

指控三：被要求签署一份抹去Alpöge名字的论文

最炸裂的指控：Buckmaster声称OpenAI提出了多个”方案”，其中一个是由Buckmaster发表论文宣告Navier-Stokes被内部OpenAI模型解决，但Levent Alpöge的名字不在其中。

Bubeck在社交媒体上强烈否认。Sam Altman也亲自下场辩护。但三条指控，每一条都触及了数学界最核心的伦理规范：独立性、透明度、署名权。

数学界的优先权规范，在AI时代能活下去吗？

数学界对”优先权”（priority）的执着，有一个深层功能理由。

优先权决定荣誉，而荣誉是数学家公开分享研究的核心动力。如果没有明确的发现归属，数学家就没有动力在证明完成前公开分享思路——这会严重减慢整个领域的进步。Buckmaster和Alpöge公开发布了他们的进展，遵循了这个规范；而OpenAI在得知后加速，撞到了这个规范的核心边界。

但AI的出现，让这套规范面临三重新挑战：

第一，”工具”和”创造者”的边界消失了

过去，AI是工具（如Mathematica、Lean）；人类数学家是创造者。这个边界清晰。但当OpenAI使用一个”比GPT-6 Astra更强大得多”的内部模型，1万个智能体并行，人类监督者无法逐一理解每一步推导，“工具”和”创造者”的边界就彻底模糊了。

谁是”发现者”？那个内部模型？OpenAI？Bubeck团队？算力投入的决策者？

第二，训练数据污染是一个无法自证清白的问题

即使OpenAI没有”主动”查看Buckmaster的Codex日志，他们的模型仍然训练在海量的数学资料上——包括arXiv预印本、StackExchange答案、数学论坛讨论。如果Buckmaster曾在任何地方公开讨论过相关思路，这个信号极有可能进入了训练数据。

这不是指责，而是一个结构性的不可能：任何现有的AI系统，都无法自证其证明的”原创性”。

第三，”赶发”在AI时代变成了”用钱砸”

传统学界的赶发，依赖个人才华和运气的叠加。而AI时代的赶发，可以用算力购买。OpenAI只需要决定：把多少台H100集群指向这个问题，以及在哪个时间节点上推。这不是数学竞争，这是资源竞争。

这个不对称，从根本上打破了数学界的竞争规范——因为规范建立在”参与者的资源大体上是可比的”这个默认假设之上。

这个证明，真的成立吗？

独立验证仍在进行。

Lean形式化的优点是：机器可以逐步验证证明的每一步逻辑是否自洽。但”Lean正确”和”数学正确”之间，还有一步：数学家需要确认，人类的数学概念被正确地”翻译”成了Lean的形式化语言。

目前已有独立数学家开始审阅这个证明。OpenAI团队的Ven Chandrasekaran（他本人是数学家）指出，OpenAI的解法与Buckmaster/Alpöge的解法”在本质上是不同的”——这有助于厘清优先权，但也意味着双方都需要独立验证。

如果证明成立，这将是数学史上第一个由AI系统主导解决的千禧年大奖问题，也将打开一个新的问题：Clay数学研究所的百万美元奖金，应该颁给谁？

规则正在被打破，但新规则还不存在

arXiv现任主任已公开表示，将召集特别工作组讨论AI参与的数学发现的发表规范。美国数学学会（AMS）宣布将在今年年会上举行专项讨论。但到目前为止，没有任何规范被确立。

与此同时，OpenAI发出了一个更明确的信号——在宣告Navier-Stokes解法的同时，他们写道：”我们认为让世界了解AI进步的速度和即将到来的模型的预期能力是重要的。”

这句话几乎是白纸黑字地告诉所有人：GPT-7或更强的模型即将到来。Navier-Stokes证明，与其说是纯粹的数学成就，不如说是一张能力演示的名片——写给下一轮融资的投资者，也写给所有对AI能力持怀疑态度的人。

从Grothendieck独自革新代数几何，到Perelman闭门七年证明庞加莱猜想——数学史上最伟大的工作，往往是孤独的、拒绝功名的。

而OpenAI在88小时内，用数百万美元和1万个智能体解决了一个百年难题。

两者之间的距离，不是数学的距离，而是人类的距离。

参考资料

  1. OpenAI. “On the Navier–Stokes Millennium Prize Problem.” September 8, 2026. https://openai.com/index/navier-stokes-solution/
  2. Knight, Will; Zeff, Maxwell. “OpenAI Just Claimed a Huge Math Discovery. Some Academics Are Crying Foul.” Wired, September 8, 2026. https://www.wired.com/story/openai-navier-stokes-math-discovery-academics/
  3. Buckmaster, Tristan. Statement on Navier-Stokes priority claims. CIMS NYU, September 8, 2026.
  4. Clay Mathematics Institute. “Navier-Stokes Equation: Millennium Prize Problem.” https://www.claymath.org/millennium/navier-stokes-equation/
  5. Bubeck, Sebastien. Response on X (formerly Twitter), September 8, 2026.

附：什么是Lean，以及为什么形式化证明很重要

Lean是一种交互式定理证明编程语言，最初由微软研究院开发。它允许数学家把数学证明”翻译”成机器可逐步验证的形式化语言——就像把一篇人类可读的数学论文，变成一段可以被计算机从头到尾检验每一步逻辑的代码。

在Lean验证中，每一个”步骤”都必须以严格的形式逻辑来支撑，不允许”显然成立”或”读者自行验证”。这意味着：Lean形式化通过≠就是数学上正确。它排除了人工引入的逻辑漏洞，但前提是翻译本身是准确的。

OpenAI完成的Lean形式化，是这个证明可信度的重要背书。但它不能替代数学家对”概念翻译”的审核——而这个审核，还需要时间。

Buckmaster和Alpöge自己也在用AI（Claude和Codex）辅助数学研究。他们用的是更传统的方式：AI辅助验证和自动化辅助推导，但数学核心推理仍由人类数学家完成。

这个对比，精准反映了2026年AI与数学关系的真实图谱：不是AI替代数学家，而是AI开始以不同的方式”参与”数学创造——有时作为辅助，有时作为主导，这两种形式之间的边界正在消失。

而边界消失之处，也是规则最混乱之处。这场争议，不会是最后一场。