纳维-斯托克斯被 AI 证出来了？
9 月 8 日，OpenAI 公布自家内部模型做出了纳维-斯托克斯方程"有限时间爆破"的证明——这是克莱数学研究所七个千禧年难题之一，挂了 26 年、悬赏 100 万美元。数字给得很硬：约 1 万个 Agent 并发协作，88 小时拿到答案，之后用 GPT-6 Astra 做 Lean 形式化验证又花了 17 小时；整个项目发了 490 万条消息、消耗约 3000 亿输出 token，其中纳维-斯托克斯单题 270 万条消息、约 1300 亿 token。按 GPT-6 Astra 公开 API 价折算，3000 亿输出 token 大约 1500 万美元——内部模型成本没公布，这只是外部估算。

先说证明本身。走的是"反例"路线：存在光滑初始条件，让方程的解在有限时间内速度无界增长，对应克莱官方问题描述里的 C、D 两条。证明的 Lean 证书已开源（openai/NavierStokesAndEuler，1,630 星，Apache 2.0），任何人装了 Lean 就能自己 lake build 跑一遍。
再说争议，这部分比证明更值得看。NYU 数学教授 Tristan Buckmaster 与 Anthropic 研究员 Levent Alpöge 合作了近一年，主要用 Claude 和 Codex，8 月 15 日取得突破。OpenAI 自己的说法是：9 月 1 日听到"两个千禧年难题被解决"的传闻后启动项目。它承认对方在 forced Euler 问题上的优先权，也主动联系了双方；但按 Buckmaster 公开的书面说明，OpenAI 明确不邀请 Levent 联合署名。关于训练数据，OpenAI 写的是"没有访问任何具体用户数据"，同时留了一句：无法排除这些人的使用数据经脱敏后帮助过模型改进。

所有数字都来自 OpenAI 自家博客，未经同行评审；Lean 能验证的是形式化本身成立，不等于数学界已经接受这个结论；成本是外部按公开价估算，不是官方数据。我的判断是，这件事真正的分水岭不是"AI 能不能做数学"，而是"谁来独立复核"——对做研究的人，实际动作就是等第三方把 Lean 证书重跑一遍、等数学社区给出评审，再决定要不要引用。

AI 生成的证明需要独立复核才算数的话，你更信"机器自检"，还是"人再读一遍"？