OpenAI 解出纳维-斯托克斯方程？数学界为何质疑
OpenAI 说智能体群 88 小时解出纳维-斯托克斯方程，交了 166 页 Lean 机器可验证的证明，数学界却没鼓掌：优先权之争、单独署名传闻、自认不能排除用户数据帮到了模型。这期讲清该看哪三样才敢信。
这期讲了什么
- 纳维-斯托克斯方程描述水和空气怎么流，是 Clay 研究所七道千禧年难题之一，解出一道给 100 万美元；OpenAI 自称智能体群 88 小时拿到解，附 166 页论文——这些数字只有 OpenAI 一家在说
- Lean 机器验证只保证推理逐行没漏洞，管不了想证的是不是这件事，也管不了有没有人读懂：机器点了头，人还没点头
- 优先权争议：Buckmaster 和 Alpöge 私下做了一年、8 月 22 日过了机器检查，OpenAI 9 月 1 日才组队；Buckmaster 声明里说对方提出让他单独署名、把 Anthropic 的合作者剔出去，OpenAI 的 Bubeck 否认
- 最硬的一层是数据：两位数学家这一年干活的主力工具是 OpenAI 的 Codex，OpenAI 自己承认「不太可能但不能排除」用户数据帮到模型；Thom 一句扎心话：去标识化能去掉名字，去不掉数学想法的内容
- Clay 研究所把这道题从未解列表移除但仍标 Active，只说「看来已被解决」、流程刻意不着急——发表满两年且学界普遍接受才发奖
文字稿
OpenAI 宣称 88 小时解出百年难题
OpenAI 宣布，它解出了一道挂了很多年的数学难题。解题的是一群 AI 智能体，跑在内部更强的一版模型上。你大概也刷到了，第一反应跟我差不多：又来了。可这次数学圈里没人鼓掌，先皱起了眉，这很少见。
围绕这件事的声音几乎是对立的：有人说 AI 又赢了，有人说这根本不算数。我以前也站「又赢了」那边，直到发现自己根本没法判断。一份没人独立复核过的证明，为什么能让一个百年数学难题算解开了？
先看这道题在问什么。纳维-斯托克斯方程，描述的是水和空气怎么流，天气预报、飞机设计都靠它算。留下来的问题是：水流里的漩涡会不会越转越猛，最后炸掉？这是千禧年难题之一——Clay 研究所列的七道题，解开一道给一百万美元。
OpenAI 自己的说法是：九月初才听说有人在攻这道题，当天就把智能体群放上去跑，88 小时之后拿到解，还发了一份交给机器逐行检查的材料。我核过那份论文，一手 PDF 是 166 页。这些数字，只有 OpenAI 一家这么说，没有第三方独立统计过。
Lean 机器验证，为什么数学界还是不认
数学圈不买账的第一层原因，就在那份材料上。那套材料叫 Lean，是个做机器验证的工具：你得把证明写成它能读的形式，Lean 逐行检查推理里有没有漏洞。它只管推理对不对，管不了你想证的到底是不是这件事，也管不了有没有人读懂。所以现在是：机器点了头，人还没点头。
纽约大学的数学教授 Buckmaster 在声明里说，他和 Anthropic 的研究员 Alpöge 私下做了一年，八月出了结果，八月二十二号过了机器检查；OpenAI 是九月一号才开始组队的。所以争的不是谁先做出来，而是优先权：知道别人快做出来了，再集中力量抢发，算不算犯规。
Buckmaster 在声明里还说了一件事：九月六号那通电话里，对方提出可以让他单独署名发表，把在 Anthropic 上班的 Alpöge 从作者里去掉。他用的词是贿赂，也写明他不是在指控谁，只是陈述听到了什么。OpenAI 那边，Bubeck 否认要求删掉对方名字。
最硬的一层是数据。OpenAI 在自己的公告里承认过：不太可能，但不能排除，他们用产品时产生的、去掉身份信息的数据，帮到了模型。而这两位数学家这一年干活的主力工具就是 OpenAI 的 Codex，草稿全在对话里。Buckmaster 说他问过训练的事，没得到回答。德累斯顿的教授 Thom 一句话最扎心：去标识化能去掉名字，去不掉数学想法的内容。
Clay 研究所还没盖章，你该怎么看 AI 的大成果
Clay 研究所也没说这就是定案。它把这道题从官网的未解列表里拿掉了，可上面还标着 Active——仍然活跃。声明里只写：这道题看来已经被解决，流程刻意不着急。规矩是发表满两年、学界普遍接受才给奖。所以现在就说官方确认解开，太早了。
这整件事跟你有什么关系？往下缩一层就是：AI 交给你一个东西，你能验收吗？验不了，你签下的就是一个看不懂的字。
下次刷到 AI 报出大成果，先别急着转，先查三样：有没有人能独立复核、用没用你的数据、有没有人真读懂。你自己呢——AI 交给你的东西，你会去找出处，还是看着像对就直接用？
常见问题
纳维-斯托克斯难题是什么？
它描述水和空气怎么流动，天气预报、飞机设计都靠它算。留下来的问题是水流里的漩涡会不会越转越猛最后「炸掉」。这是 Clay 研究所列的七道千禧年难题之一，解出一道奖金 100 万美元。
Lean 机器验证过了为什么数学界不认？
Lean 只逐行检查推理有没有漏洞，管不了你想证的是不是这件事，也管不了有没有人读懂。再加上两位数学家先做了一年、涉及优先权和数据争议，所以是机器点了头、人还没点头。
Clay 研究所承认 AI 解出来了吗？
没有定案。它把这道题从官网「未解」列表移除但仍标着 Active，声明只说「看来已被解决」、流程刻意不着急。规矩是发表满两年、学界普遍接受才给奖，现在说官方确认解开太早。
AI 报出大成果该看哪三样？
一查有没有人能独立复核，二查训练用没用你的数据，三查有没有人真读懂。更缩一层问你自己：AI 交给你的东西，你能验收吗？验不了，签下的就是一个看不懂的字。