88 小时解出百万美元难题，代价是功劳没算清
Hello，我是飞飞。
四天前我刚写过一篇，说 Anthropic 让 AI 把费马大定理的证明翻成 Lean，结论落在一句话上：AI 说证出来了不算数，编译器说了才算。当时我觉得那已经是 AI 碰数学最猛的一次。这个纪录只活了三天。
9 月 8 号，OpenAI 官宣：一组智能体用一个还没发布的模型，解出了 Navier-Stokes 的 blowup，七大千禧年难题之一，悬了 90 多年，Clay 研究所的奖金是 100 万美元。同一个时间窗里，NYU 数学家 Buckmaster 发了一份四页声明，指认这场解法的起点是走漏的消息。三方各说各话，至今没对上。
证明没公开，功劳的账也没算清。这篇我把它当一起进行中的事故讲：谁的责任我不判，先把我核到的数字和三处对不上的口供摆出来。
先说解出了什么
Navier-Stokes 是描述流体运动的方程组。这道题问的是：初始光滑的流动，会不会在有限时间里爆掉，速度变成无穷大。blow up 说人话就是数学式子里算出了无穷大。这一半要是成立，光滑解永远存在那半就不成立。数学内容我只交代到这，再深我也插不上话。
OpenAI 的跑法，数字都标了出处。约一万个 agent 并发，9 月 1 日开跑，88 小时后拿到证明；再花 17 小时，由已经发布的 GPT-6 Astra 把证明翻成 Lean 验证。
消息和 token 的账要分开看：全部尝试过的问题合计 490 万条消息、约 3000 亿输出 token，Navier-Stokes 本体占 270 万条消息、约 1300 亿。这个区别各家转述都在丢，我自己核的时候也差点混过去。
成本有两个口径。OpenAI 的 Bubeck 估算「数百万美元」；Simon Willison 按公开牌价自己算了笔账，3000 亿输出 token 按 Astra 计价约 1500 万美元，注明内部模型的真实成本结构未知。两个都是估算，你当量级看。
还有一个前提必须写明：这份证明到现在没有公开，没有经过独立数学家审阅，Buckmaster 本人说他没见过。
一条走漏的路线
声明这边的时间线是这样的。Buckmaster 和 Anthropic 研究员 Alpöge 合作近一年，站在 Córdoba 和 Martínez-Zoroa 几年铺垫的构造路线上，用 Claude 和 OpenAI 的 Codex 往前推。8 月 15 日，他们解出了 Euler 方程的 blowup，8 月 22 日在 Lean 上验证通过。
声明里他专门补了一句学术操守：这套路线的功劳属于 Córdoba 他们俩，还说 Martínez-Zoroa 配得上菲尔兹奖。
然后是走漏。按 Buckmaster 的说法，两人未发表的工作信息经由 Codex 会话到达了 OpenAI。9 月 3 日起，对方多次约通话。9 月 6 日，电话通了。他是在这通电话里才知道，OpenAI 那个还没发布的模型，正沿着他们走了近一年的那条「强迫」路线往前推。强迫是个数学行话：往方程里加个外力项，把原本撑得住的解一步步逼到爆掉。两天后，声明和三篇 Lean 验证过的论文被他贴了出来。
从消息走漏到一家公司宣布解出千禧年难题，前后一周左右。
声明的几个细节值得单看，它们拼出来的是一个最不像来碰瓷的人：合作是纯个人的，没拿 NYU 和 Anthropic 任何机构授权；用了一年多 LLM，最近才碰 Astra，而且只让它写 writeup 和审计论证。把 AI 用得这么克制的人站出来说别人抢跑，这话的分量就不一样了。他写的头一条 LLM 生成证明，「是我这辈子读过的最吓人的证明」，8 月 22 日在 Lean 上验过了，他照样敢用。
三篇论文里 Euler 那篇的成稿，他公开道歉说「只能被描述为 AI slop」，原因是被外部因素赶着发文。数学家的署名底下压着一篇自己都嫌 AI 味重的论文，这才是这场架里最讽刺的一帧。
那三篇论文本身是真成就。菲尔兹奖得主陶哲轩公开评价说是 remarkable achievement，还说他看不出把同样方法推到完整 Navier-Stokes 有什么障碍。
三处对不上的口供
争的是三件事，每件都是两个版本。
路线。OpenAI 的口径是模型先解出了无强迫 Euler 的 blowup，再推进到 Navier-Stokes，以此自证走的是独立路线；Buckmaster 认定对方走的正是他们那条强迫路线。哪边是真相，现在没有裁决，连 Reddit 上的技术社区都在等双方的证明文本对质。
数据。OpenAI 声明说「没有访问任何特定用户数据来解这个问题」。但同一份声明里还有一句，被 Willison 全文加粗的那句：不能排除来自用户使用行为的去标识化数据，帮助改进了我们的模型。前半句说得很满，后半句留了条缝。
署名。Bubeck 贴出聊天记录，自证提过让 Buckmaster 团队先发；Buckmaster 的版本是，方案的条件之一是把 Alpöge 从作者名单里去掉，因为 OpenAI 不喜欢 Anthropic 的隶属关系。Altman 也回应了，称对方手里只有 Euler 的结果、双方协调失败，这条我只有中文摘要口径，原推没核到。
Quanta Magazine 的定调最老实：对话的各方在讲不同版本。
三件事我一件都不判。措辞上你也看出来了，每个指控我都挂了名字：谁说的、谁贴的记录、谁否认。原话都在，可信度你自己掂量。
编译器只算了一半
四天前那篇的结论，这回要打个对折。Lean 验证确实过了，17 小时，Astra 做的，这个环节无可挑剔。可「编译器说了才算」还有后半句：验证过的东西要摊开来给人看。
四天前 Anthropic 那回，1300 万行 Lean 全文摊开，只认三条公理，任何人都能逐行查。这回 Lean 证书在谁手里、外部能不能独立复跑，外界一概不知。证明全文没公开，独立数学家没审过，Clay 研究所的领奖条件是论文发表加广泛专家接受，最少以月计。
这道验证门两边都在守。Buckmaster 自己那篇 hypo-dissipative Navier-Stokes，就因为 Lean 还没跑完，宁可压着不发。数学家在守，厂商也知道自己得守，只是厂商守到一半就去开了发布会。
吵闹里最值钱的一句
这场架里我认为最值钱的一句，出自 Willison 的一个类比。安全圈有条老话：如今有 bug 的传闻，就够找到漏洞利用了。他问数学是不是也一样，只要某个难题存在未发表解法的传闻，就足以触发一场几百万美元的 agent 竞赛。传闻本身成了攻击面。
再往下是他的假设性问题，我念一遍你就能掂出分量：你用 ChatGPT 啃一个难题，你的工作会不会通过训练，让下一个模型替别人抢先完成？OpenAI 那句「不能排除」，等于没否认这条通道。每个往对话里倒真问题的人，都在往通道里流东西。
我自己的一点一手体感对得上。我审 agent 交的活靠三样：git diff 逐行过、测试跑没跑、输出对不对。上个月迁移一个 7000 多行的老项目，agent 把一个叫 isLiability 的字段悄悄改没了，编译通过、测试也过，靠流水线里一道对抗校验关卡才捞回来。让我自己肉眼读那几千行 diff，这个 bug 八成混过去。[素材库:AI-Agent-与工作流]
多智能体这边我还攒下一条账：agent 一多，烧的 token 是普通对话的十几倍，任务怎么分、状态怎么记、错了谁来兜底，全是真金白银换来的坑。所以一万个 agent 干 88 小时这件事，让我停下来的不是钱，是它的目标：抢一道题的优先权。原来「谁先证出来」这件事，现在也有了报价。
这事还在进行中。我留三个后续观察点：证明全文什么时候公开，独立数学家验不验得过，Clay 研究所认不认。有动静我接着写。
轮到你了：你把没解决的真问题丢给 AI 的时候，想过它在对方训练数据里的下场吗？如果厂商能拿着你用它的痕迹抢先一步，你还敢不敢把压箱底的问题丢进去？评论区聊聊，你的线划在哪。