事件与背景

9 月 8 日，纽约大学柯朗所数学家 Tristan Buckmaster 发布个人声明 PDF，随即登顶 Hacker News（606 分 / 324 评论，本文截稿时仍居第一）。声明宣布他与哈佛大学、同时任职 Anthropic 的 Levent Alpöge 合作，公开三个结果：带光滑外力的不可压多孔介质方程、Boussinesq 方程、以及 3D 不可压无粘 Euler 方程的有限时间爆破（构造在有限时间内发展出奇点的光滑解）；其中 Euler 与 Boussinesq 的关键证明在 8 月 15 日取得、8 月 22 日首个 LLM 生成的证明即通过 Lean 形式化验证。他们还相信 hypo-dissipative Navier–Stokes 的爆破也成立，但因 Lean 验证未完成而暂不发布。

最重磅的是 LLM 在其中的角色。声明明确：纲领并非 LLM 提出——基本想法来自 Diego Córdoba 与 Luis Martínez-Zoroa 多年推进的「受迫爆破」研究路线，Buckmaster 直言后者「值得一枚菲尔兹奖」；两位作者是「用 LLM 把这一纲领推到了光滑外力与 Euler 方程」。全程使用了 Anthropic Claude、OpenAI Codex（尤其是 GPT-5.6 Sol），以及更晚加入、仅用于撰写与审计的 Astra。Buckmaster 的核心判断是：「一位数学家和一个 LLM 现在可以一个月做完这一切」才是重点，这是数学的 Deep Blue–Kasparov 时刻，对学生培养、署名、评审与「什么值得一个人付出一生注意力」都将产生冲击。他自嘲 Euler 论文的成稿「只能称为 AI slop」，因为舆论压力迫使他们仓促公开。

同一天（北京时间 9 月 9 日凌晨 01:13 收录于 HN），OpenAI 官网发布《On the Navier–Stokes Millennium Prize Problem》（532 分 / 370 评论）。需要明确标注：本文写作时该页面被 Cloudflare 拦截（curl 403、浏览器验证无法通过），OpenAI 正文内容未能直接核实，以下情节均出自 Buckmaster 声明这一方叙述——9 月 3 日已有「Anthropic 解决了重大开放问题」的传言，且 Alpöge 收到「进展信息已传至 OpenAI」的提示，Buckmaster 遂主动邮件 OpenAI 数学家；9 月 6 日他与 OpenAI 的 Sébastien Bubeck 通话，被告知其内部模型产出了「受迫 Navier–Stokes 在 R³ 与 T³ 上的有限时间爆破（光滑外力，对应 Fefferman 表述的选项 c/d）」的约 100 页证明，他未亲见；OpenAI 先后提出两个方案——双方各自发布、或由他单独署名撰写该 NS 结果（并两次要求把就职于 Anthropic 的 Alpöge 移出作者名单），均被他拒绝，随后出现「为什么要毁掉你的职业生涯」「如果我不想对你客气，我就不必客气」等言论；他询问模型是否接触或训练于存有两人全部草稿的 Codex 会话，得到「未查询用户数据」的答复，再追问训练相关则未获回答。Buckmaster 反复声明：「我不是在指控任何人，只是在陈述被告知了什么、何时、被提议了什么。」

需要划清事实边界：Euler 爆破与「受迫 NS 爆破」都不是千禧年问题本体（无外力 Navier–Stokes 的正则性），而是该方向上被普遍视为关键路径的邻接突破——媒体若写成「AI 解决千禧年问题」即为标题党。

来源：

• Tristan Buckmaster 个人声明（PDF，原始出处）
• HN：Navier-Stokes – Tristan Buckmaster（606 分 / 324 评）
• HN：On the Navier–Stokes Millennium Prize Problem（532 分 / 370 评）
• OpenAI 官网文章（⚠️ Cloudflare 拦截，正文未核实）

为什么现在重要

1. 研究节奏发生量级变化：一个月 vs 一个人一生。 从「rough forcing」到「光滑外力 + Euler」的跨越，两位学者在 LLM 帮助下用约一个月完成并 Lean 验证；过去这类结果意味着顶尖团队数年的攻坚。影响判断：定理产出的瓶颈正在从「想得出」转向「验证得了、讲得清」，数学家的稀缺性将重新定价。
2. 「LLM 生成 + Lean 验证」成为可信闭环，AI slop 有了安全网。 声明坦然承认人不可读的模型输出，但机器可核验的形式化证书补上了可信度——「可读性差」不再等于「不可信」。影响判断：形式化验证工具链（Lean/mathlib）会从学术冷门变成 AI 科研的基础设施，正如测试之于软件工程。
3. 用户会话数据是否进入厂商竞争性研究，第一次被公开拷问。 两位作者把全部草稿放在 Codex 会话里，而 OpenAI 恰在获知其进展后数日内宣称内部模型得到同一路线结果；「模型是否在用户数据上训练」的追问没有答案。影响判断：无论真相如何，用 coding agent 存放敏感 IP 的数据治理条款将成企业采购硬指标。
4. 数学成为 labs 之间新的竞赛场，且力量极不对称。 一方是自费（包括付给 OpenAI 的大额账单）的个人合作，一方是内部模型 +「疯狂量级」算力 + 整支团队；而关键人才 Alpöge 恰在 Anthropic 任职，署名之争直接撞上实验室墙。影响判断：学术界与工业 labs 围绕成果归属的摩擦会高频化，需要新的披露与仲裁规范。
5. 它对「AI 只能做工程、不能做数学」是一次正面证伪。 即便纲领归功于人，把纲领推到完成的关键证明由 LLM 生成并经 Lean 验证，是迄今最接近「AI 参与前沿数学发现」的公开案例。影响判断：2026 年剩余时间的头条会密集出现「XX 被 AI 攻破」类消息，读者需要一套含验证状态的鉴别框架。

工程师/产品人今天能做什么

1. 核查你 coding agent 工作区的数据边界。 若 Codex/Claude 等会话内存有未公开草稿、代码或 IP，本周内逐条核对厂商的数据使用与训练条款，重要项目开启「不用于训练」开关或迁移到隔离工作区——本事件给出了现成的风险剧本。
2. 为团队引入「双工件」交付标准。 凡 LLM 深度参与的关键结论，必须附带机器可执行/可验证工件（测试、复现脚本、证明），如同 Lean certificate 之于数学证明：可读文本会美化，可执行验证不会。
3. 跑一次「AI 辅助形式化验证」试点。 用你手上最强的模型（本次实测有效的包括 Claude 与 Codex/GPT-5.6 级）证明 mathlib 中一道中等难度引理，度量「自然语言论证 → Lean 4 通过」的完整周期，为算法与数学研发管线评估成本。
4. 把 AI 贡献声明写进内部论文与评审模板。 谁提出纲领、谁生成证明、谁验证、谁撰写、用了哪些模型与算力——Buckmaster 声明本身就是一份可复用的披露样板，先于期刊要求落地。
5. 管理者为「人机协作科研」预留预算与政策。 个人研究者自费对抗实验室算力的差距正在拉大；明确员工用自购/自备模型做研究时的知识产权归属，避免下一个 Alpöge 式困境。

待观察

1. Buckmaster–Alpöge 的论文与 Lean 证书正式公开（声明称「即将」），以及 Euler/NS 专家社区的独立核查结论——这是判断「LLM 是否真正推进了前沿数学」的第一块试金石。
2. OpenAI 官网文章正文与细节（当前被 Cloudflare 拦截）；其内部模型的受迫 NS 爆破证明是否会公开、是否附带 Lean 验证、与 Buckmaster 所述版本是否一致。
3. 「模型是否在用户 Codex 会话数据上训练/可访问」是否会得到正式回应；「Anthropic 解决重大开放问题」的传言源头与 OpenAI 侧的说法（截至本文截稿，OpenAI 未公开回应声明）。