数学家：OpenAI 没读懂自己那道证明

一道千禧年难题的证明摆在那里，机器能逐行检查每一步。但作者在开头写的「我们用了谁的方法」，一个月后被同行指出是错的。

这不是证明错了，是讲错了。两者的差别，决定了我们该怎么看待 AI 做出的研究。

一、发生了什么

9 月 8 日，OpenAI 公布了一份 166 页的纳维-斯托克斯问题解答。这是克雷数学研究所七道千禧年难题之一，悬赏一百万美元。证明由内部大模型产出，同时被写成了 Lean 代码。Lean 是一种形式化语言，能把每一步逻辑交给机器校验。

发布时，OpenAI 的说法是：证明沿用了西班牙数学家迭戈·科尔多瓦和路易斯·马丁内斯-索罗阿的路线。这个说法引发了一场公开冲突。纽约大学的特里斯坦·巴克马斯特和 Anthropic 的莱文特·阿尔珀格过去一年一直在用大模型推进这条路线，他们认为 OpenAI 的工作建立在自己的进展之上。巴克马斯特还称 OpenAI 曾试图用利益和压力阻止他公开质疑，OpenAI 否认使用了他们的数据。

一个月后，据《科学美国人》10 月 13 日报道，多组正在逐页读这篇论文的专家得出了相反结论：证明并没有沿用它声称的那条路线。洛桑联邦理工学院的数学家贡萨洛·曹-拉博拉说得很直接——看到细节，就是另一套方法，相似只在表面。

参与这项工作的智能体数量是 1 万个，累计跑了约 88 小时、消耗 1300 亿词元。OpenAI 研究员诺姆·布朗说，没人真正知道这套多智能体编排贡献了多少，他估计不到一成；真正起作用的是基础模型本身能长时间磨一个任务。

克雷数学研究所从论文发布起就在审阅。普林斯顿高等研究院的卡米洛·德莱利斯说，这件事恐怕不会有事实层面的结论，因为大模型的推理过程是黑箱。

10 月初，OpenAI 又向社区放出了约 400 项结果。

二、跟你有什么关系

如果你是做研究的：这份材料提醒你，AI 给出的「方法说明」不能当作方法本身。你要复现的是代码和中间步骤，不是摘要里的那段话。

如果你在用 AI 做工程判断：结论正确、过程可验证、作者理解自己在做什么，是三件独立的事。采购或评审时，要把它们分开问。

如果你只是读者：这条新闻最容易被读成「AI 又解决了一个大问题」。更准确的读法是，AI 产出了一个结果，而人类花了一个月才搞清它到底怎么来的。

三、怎么判断一个「AI 做出来的成果」

1. 先确认验的是什么。Lean 校验的是写进代码的那条命题。这条命题和原始问题是否严格对应，需要人读形式化定义，机器不会替你判断。

1. 让对方给出可复现的路径。不是「我们用了某方法」，而是每一步对应哪段代码、哪个引理。说不清路径，就还停留在「结果摆在这里」。

1. 看算力账单。1 万个智能体、88 小时、1300 亿词元，这是一次昂贵的搜索。知道成本，才知道它能不能再来一次。

1. 看争议能不能被裁决。数学争议通常靠同行读证明解决。这次卡在黑箱上：即使所有专家都同意「方法不同」，也没人能证明训练数据里有没有别人的东西。

1. 把「未确认」写进结论。克雷研究所还没认定，论文也还在被拆读。在这个阶段把它说成「难题已解决」，是替审稿人下结论。

四、三个别信的说法

「AI 独立解决了千禧年难题。」 目前能确认的是：OpenAI 发布了一份 166 页的证明，形式化部分可机器校验，克雷研究所在审。不能确认的是：它是否构成对该问题的完整解答、是否独立于前人工作。奖项认定权在研究所，不在发布会。

「Lean 通过了，数学界就认了。」 Lean 检查的是逻辑步骤有没有漏洞，不检查这条命题值不值得证、是不是原题。形式化写错一个条件，机器照样通过。这也是为什么专家要花一个月重读，而不是跑一遍校验器就结束。

「1 万个智能体是成功的关键。」 连 OpenAI 自己的研究员都估计，多智能体编排的贡献不到一成。规模看起来很震撼，但这类系统还没有经过系统的对照实验——没人算过 1000 个智能体要跑多久。把功劳记在「 swarm 」上，是把工程手段当成了科学突破。

五、一句话结论

机器能证明，和人能解释，是两种能力；这次出问题的是后者。

信息来源

• The Decoder：《Mathematicians say OpenAI doesn't understand its own Navier-Stokes proof》，2026 年 10 月 17 日：原文
• Scientific American：《OpenAI's blockbuster math proof isn't what you think it is》，2026 年 10 月 13 日：原文

功能与价格以官方公告为准。本文写于 2026 年 10 月 18 日。