OpenAI 的纳维-斯托克斯方程连续剧，播到第四幕了。
第一幕是庆功：9 月 8 日，OpenAI 宣布模型用一份 166 页的证明，拿下悬赏 100 万美元的千禧年难题。第二幕是控诉：庆祝的香槟还没凉，就有数学家甩出一份措辞激烈的 PDF，指责 OpenAI 截胡自己的课题。第三幕是对峙：10 月 6 日 722 份数学手稿一次砸出，#人类数学家联合抵制 OpenAI# 冲上热搜。10 月 16 日，《科学美国人》的追踪报道让第四幕上了头：OpenAI 交出的证明，根本不是它当初宣布沿用的那条「西班牙路线」，而且连 OpenAI 自己都没搞懂，自家模型到底证了个什么。量子位
一路追更的人都知道，这早就不是"AI vs 数学家"这么简单的故事；半路刷到热搜点进来的，这篇帮你把时间线、讹传和真正的看点一次排清。
一、先把一个月连续剧排成时间线
9 月 7 日：一位数学家公开发难，指责 OpenAI 试图截胡他的研究课题，"AI 抢发"争议第一次进入公众视野。科普中国
9 月 8 日：OpenAI 官宣 NS 成果，未公开的内部模型约 1 万个 Agent、跑了 88 小时，产出 166 页证明外加 Lean 形式化代码；高管反复强调，证明沿用了西班牙数学家 Córdoba 和 Martínez-Zoroa 的研究路线。中新网
9 月 11 日：包括陶哲轩在内的 25 位菲尔兹奖得主联名发表《人工智能在数学中的严重错位》。中国新闻周刊
10 月 6 日：OpenAI 一次性放出 722 份数学手稿，归为 372 组研究成果，来自 4000 多个测试问题，每项成果平均消耗约 3 小时 ChatGPT Pro 量级的算力。
10 月 7—9 日：“人类数学协会”（AHM）宣言流传开来，成员宣言不会发表完全由 AI 生成的论文，并呼吁数学界停止与 OpenAI 合作，话题随之引爆。
10 月 16 日：《科学美国人》援引多个正在啃这份证明的专家团队：OpenAI 最终证明里构造外力的方式与西班牙路线完全不同。EPFL 数学家 Gonzalo Cao-Labora 话说得很直："深入研究具体细节之后就会发现，这是一种不同的方法。"普林斯顿高等研究院的 Camillo De Lellis 补了一刀：这场归属争议，恐怕很难有明确的事实性结论。量子位
换句话说：模型把题做了，公司没看懂它是怎么做的，就端上来了。
二、热搜上的版本，至少有五处是加戏
反转 ≠ 证明被推翻了。 反转的是"沿用了谁的方法"，不是"证没证对"。这份证明附带 Lean 形式化代码，计算机可以像跑代码一样逐行核验逻辑，目前没有任何数学家宣布它是错的。
“陶哲轩带头宣战、率人类数学家抵制 OpenAI”，是两件事拼在一起的。 陶哲轩是 9 月 11 日 25 位菲奖得主联合声明的签署人之一；AHM 宣言是他转载到自己博客的——而 AHM 那个"不发全 AI 论文"的成员宣言里，他自己并不在列。 数学界最积极拥抱 AI 的顶尖学者之一，在传播链里被剪成了反 AI 起义军领袖。科普中国
“AI 解决 NS、要拿走 100 万美元”，言过其实。 OpenAI 证明的是：借助精心构造的平滑外力，流体可以在有限时间内出现爆破，符合克雷数学研究所题面允许的 C、D 两种命题形式；数学家真正在意的无外力版本至今未解决，克雷方面也从未因此宣布授奖。量子位
“722 题全部得证”，核验进度完全不一。 只有部分手稿附带 Lean 形式化证明；700 多份成果里只有 10 份公开了提示词和模型思维过程——这正是数学家集体开炮的核心：你解决了问题，但把可复现性、可理解性全留下了。
“数学家是怕失业才闹”，被数据反驳了。 追踪网站 Proofs and Prompts 收集了 100 名数学家对 OpenAI 的反应：大多数人其实惊叹于成果本身，少数的激烈反对集中在发表规范和署名机制。 吵的不是 AI 行不行，而是这套成果该怎么"交"。
三、真正的看点：形式上对 ≠ 人类懂
这场反转暴露出的，是一个比"抢发"更陌生的问题。
Lean 能检查推导是否成立，但不会告诉你这套方法为什么有效、和已有研究什么关系、能不能推广。于是出现了数学史上很荒诞的一幕：数学家正在借助其他大语言模型，来理解 OpenAI 的大语言模型写出的证明。 MIT 数学家 Henry Cohn 则用软件工程里的"技术债务"形容这批论文——正确、但难读、动机缺失、充满不必要的复杂计算，他直接称之为"数学泔水"（math slop），理由很损：从前全世界只有望月新一一份看不懂的 ABC 猜想论文，现在靠 AI，人人都能成为望月新一。量子位科普中国
陶哲轩的概括更狠：传统数学是建立在"证明稀缺"上的 Math 1.0，解题的过程本身生产理解；AI 把数学推进"证明丰裕"的 2.0，AI 解题但不生产理解——人类依然需要理解数学，却突然发现，理解本身没有一个现成的买家。科普中国
一个真实样本：MIT 教授 Dor Minzer 和两名研究生花了七年做 Unique Games 猜想相关问题，9 月 11 日听到 OpenAI 可能已经证了这道题的风声，三天内抢贴出 95 页论文，还专门道歉说写得粗糙——10 月 6 日的 722 份清单里，他们的课题赫然在列。 这不是"你不够聪明"的问题，是你得睡觉、吃饭、有情绪，而你在跟一个万亿美元公司的 88 小时赛跑。科普中国
四、这出剧，你该带走的三样东西
如果你是 AI 追剧党：以后看到"AI 攻克 XX 猜想"的标题，先问三个问题——证的是官方题面的哪个版本？有没有机器可核验的形式化？有没有第三方人类消化过？NS 这季剧情，就是"①偷跑、③缺席"的活教材。
如果你是理工科研究生或青年研究者：继续盯四个信号——克雷数学研究所会不会就 NS 作裁决；OpenAI 会不会按数学家顾问组（AGMAI）的公开建议补齐模型、提示词、思维链披露；722 手稿的 Lean 形式化比例会不会上升；以及"把 AI 证明翻译成人能懂的版本"这种工作，能不能在评价体系里换个位置——哈佛、华盛顿大学相关的两场数学教育会议，已经提出博士评估不应再拿论文发表当首要依据，“论文不是博士的意义，学生才是”。科普中国
如果你是程序员：这季剧情离你并不远，微博热评几乎能原样平移——AI 生成的代码能跑，但可读性差、维护成本后移，"技术债"是同一笔。 差别只在于：数学的债由整个学科慢慢还，你的债自己当场还。微博
这一季真正的分歧，不在人类 vs AI，而在陶哲轩和 Gowers 之间：25 位菲奖得主说，数学的根本目标是概念理解，解题只是工具；没签名的 Gowers 承认，他做数学的核心动力就是解未解之谜，如果这个梦没了，他不确定还会不会选数学。科普中国
证明可以被机器核验，意义不行。下一次反转，大概率发生在某份手稿被人类"看懂"的那天，而不是被"证完"的那天。你站哪边，评论区聊。
