9 月 8 日，OpenAI 公开了纳维–斯托克斯存在性与光滑性问题的一份证明，同时放出论文和 Lean 形式化文件。这是克雷数学研究所 2000 年设立的七个千禧年大奖难题之一，单题奖金 100 万美元。OpenAI 在公告里说，不打算申领这笔奖金。
证明由一组智能体产出，用的模型尚未发布，官方描述是能力明显强于 GPT-6 Astra。结论是流体可以从光滑的初始状态出发，在有限时间内产生奇点。
88 小时，一万个智能体
比结论更少见有人公开的是过程数字。智能体 9 月 1 日启动，9 月 5 日拿到结果，中间约 88 小时，峰值同时运行约 1 万个智能体。这一题消耗 270 万条消息、约 1300 亿输出 token；把这一轮尝试过的所有问题加起来，是 490 万条消息、约 3000 亿输出 token。按公开 API 价格折算，外界给出的估值在 1500 万美元上下。
拿到分析形式的证明之后，GPT-6 Astra 又花 17 小时把它写进 Lean 并跑完检查。形式化文件已经公开，这一层比论文本身更硬：分析领域的长证明历来难审，能在 Lean 里编译通过，至少把逻辑自洽这一关从人工审稿里摘了出去。
剩下的那一关摘不出去。千禧年难题有官方的问题陈述，一份证明算不算解决它，要看构造满足的是哪一组条件。在有数学家把整份论文读完之前，“解决”两个字先挂着。目前公开的转述里没有正面写清这套构造的外力项设定，而带不带外力项，恰好是这个问题过去二十年里最要命的分水岭。
官方公告和另一份声明
同一天还有另一半。纽约大学库朗研究所的 Tristan Buckmaster 与 Anthropic 的 Levent Alpöge 公开了他们在受迫欧拉方程等三个方程上的有限时间爆破结果，Buckmaster 另发了一份声明，讲他与 OpenAI 沟通的经过。
OpenAI 公告里的说法是：最初以为对方也解出了纳维–斯托克斯，提出联合发布，后来才弄清对方做的是受迫欧拉方程，并承认对方在那个问题上的优先权。关于数据，公告写的是研究员和智能体在对方公开之前没有通过任何途径看到他们的工作，随后补了一句——不能排除由对方使用行为派生的去标识化数据起过作用，同时强调两边的证明差异显著。
TechCrunch 9 月 8 日的报道里，Buckmaster 的说法更硬。他称自己的进展被传到了 OpenAI，对方选的路线和他一样，而”几乎没有别人在做这个”。他还引述 Sébastien Bubeck 在通话中对他说过”你为什么要毁掉自己的职业生涯”，以及”如果你不想我客气，那我可以不客气”。Bubeck 此前在 X 上否认，称流传的指控虚假且带有煽动性。两边对同一通电话的记述目前对不上。
和前几次的差别
过去一年这条线上的节点有迹可循：先是费马大定理的完整机器证明在 96 核机器上编译通过，再是 Erdős 猜想那一批，之后各家把 Lean 形式化做成了发布标配。共同点是争的是数学，附的是可复现的证据链。
这一次多出来的东西，是过程本身成了争议对象。谁先开始、谁的草稿进过谁的系统、电话里说了什么，这类纠纷在纯人类的数学圈也发生过，但过去至少能靠预印本时间戳和会议记录把顺序理清楚。当一方的工具链就是另一方的产品，时间戳这条线不再中立。Simon Willison 9 月 8 日把话说得更直白：如果我用 ChatGPT 做完了千禧年难题的一部分，我的工作有多大概率会影响到训练，让后来的模型帮别人先做完？
这个问题 OpenAI 的公告没有回答，眼下也没有哪家实验室的数据条款回答得了。
参考来源：OpenAI 千禧年问题公告、TechCrunch、CocoLoop、Simon Willison 个人博客、Tristan Buckmaster 公开声明；智能体规模、消息与 token 口径以官方公告及其转述为准，折算成本为按公开 API 价目的外部估算。