ARTICLE · 1265972
OpenAI一天交出三份科研突破:数学、计算机与物理,谁在复核
10 月 26 日,OpenAI 在主页上同时放出了三项声称属于基础科学重大突破的成果。
这三项分别切在三个最硬的领域:数学上,声称证明了调和分析中所有维度的局部光滑猜想,顺带推平了挂谷猜想和 Stein 限制猜想;计算机上,声称推翻了理论计算机科学里用了近三十年的指数时间假设(ETH);物理上,声称给出了四维纯杨-米尔斯理论以及量子色动力学(QCD)的严格数学存在性证明。
消息一出,Hacker News 榜首被直接占据,知乎热榜前三名里有两条是关于它的讨论。很多人看到标题的第一反应是:AI 是不是已经彻底接管基础科学了?
但如果把聚光灯从宣传词移开,回到学术研究最根本的一件事——同行复核,你会发现情况完全不是同一回事。这三份答卷里,有一份正在被领域开创者公开逐行审阅,有一份把卷子扔在公开网络上却无人正式认领,还有一份甚至连题目和草稿都还锁在少数几个人的抽屉里。
这三项成果现在全都只是“OpenAI 的单方声称”,没有一项经过正式的同行评审。它们各自走到哪一步,恰恰给所有人提供了一把看懂“AI 做科研”的尺子。
要看懂这些成果到底是真是假、算不算数,可以把整个检验过程拆成清晰的四层:
第一层是材料公开。论文、证明草稿、演算过程,外界能不能直接下载到,还是只能看一篇新闻通稿。
第二层是机器检查。有没有转化为形式化验证语言(比如 Lean)。Lean 就像一个极度严苛的逻辑检查器,只要你把证明形式化写进去,它能确保从前提到结论的每一步逻辑推导没有人工疏漏。
第三层是题面对不对。这往往是外行人最容易忽视的一层。Lean 只能保证“这个形式化命题确实被给出的步骤证明了”,但它根本无法判断“这个被机器证明的命题,是不是人类数学家当年想问的那个现实问题”。Lean 官方的检验工具 Comparator 在说明里写得很坦白:它只确认答案与题面代码一致,但不判断这个题面是不是你想问的问题。
第四层是独立同行的理解与公开背书。必须有真正懂行、不拿 AI 公司报酬、不签保密协议的学者坐下来逐行读懂,搞清楚背后的数学或物理直觉,并用人话讲给整个科学共同体听。
拿这四层尺子去量一下 OpenAI 刚交出来的三份答卷,它们处在完全不同的世界。
ETH:批改得最透明的一张
三项成果里,目前最接近正常科学复核流程的,是推翻指数时间假设(ETH)的那一项。
ETH 是理论计算机科学的核心基石之一。大约在 1999 年,Russell Impagliazzo、Ramamohan Paturi 以及 Francis Zane 提出了这个假设。粗略地说,它断言像 3-SAT 这样的经典难解问题,在最坏情况下不可能在“亚指数时间”内被解决。过去近三十年里,理论计算机界有成百上千篇论文将 ETH 作为前置假设,借此证明图论、计算生物学、数据库查询等领域的大量问题在计算上是极其困难的。
OpenAI 宣布的内容非常硬核:他们的内部模型在 10 月 16 日给出了一个确定性、多项式空间的算法,能够精确计算固定宽度布尔公式(CNF)的满足解个数。在 3-SAT 的情形下,该算法直接反驳了 ETH。
这个算法能让计算机瞬间变快吗?不能。按 Lean 代码里的定义,它的运行时间上界依然是 2 的超多项式次方量级(具体界为 $n \cdot (\log \log n)^2 / \sqrt{\log n}$)。它比纯粹的指数时间小了一点点,但依然极其巨大,并不是实用的快速算法,更没有直接推翻 P vs NP。OpenAI 联合创始人 Greg Brockman 随后在 X 上特意提醒了一句:“P 大概率仍然不等于 NP。”
但这份成果在验证流程上走得最规范。代码和论文在 GitHub 的 openai/math 仓库以 Apache-2.0 许可证完整开源。第二天,Lean 的机器检查就通过了。
更关键的是,它经受住了第三层和第四层的考验。Lean 代码把“算法”形式化为一台自定义的多带图灵机,把“时间”定义为机器的运行步数,连输入的编码方式都写死了。这套形式化模型到底有没有在编码层面动手脚?它与复杂性理论里人类认可的计算模型是否完全等价?这需要顶尖学者来审定。
这一次挑头复核的人,正是当年提出 ETH 的两位学者 Impagliazzo 和 Paturi,以及 MIT 的知名理论计算机科学家 Ryan Williams。Williams 在 X 上写得很克制,三人发布的公开信开篇就直言:“我们的参与不应被视作对该声称的背书。”他们公开声明:不签任何保密协议,不收一分钱报酬,并要求 OpenAI 公开该结果的全部原始数据,同时资助一场面向全学术界的专题研讨会。OpenAI 全盘答应。
前两层做完了,第三层和第四层正由这个领域最有动机捍卫它、也最有能力挑刺的人在查。这是最健康的一张卷子。
局部光滑猜想:卷子放出来了,谁来批?
第二张卷子属于纯数学领域的调和分析,它引起的学界情感震动甚至超过了 ETH。
局部光滑猜想由 Christopher Sogge 于 1991 年提出,描述的是波动在集中传播时能量衰减的极值规律。在数学上,它是一根关键的骨牌:根据经典的推导链条,一旦任意维度的局部光滑猜想被攻克,调和分析领域大名鼎鼎的 Bochner-Riesz 猜想、Stein 限制猜想以及挂谷(Kakeya)猜想整条链条将被全线解决。
为了这串问题,几代数学家耗尽心血。此前人类的最前沿进展,是 2019 年 Larry Guth、王虹和张瑞祥证明了二维情形;2025 年,王虹与 Joshua Zahl 证明了三维集合版挂谷猜想,王虹这项工作被普遍认为具备菲尔兹奖级别的分量。在 Hacker News 上,有研究者直接发问:“如果没有王虹之前做出的铺垫,OpenAI 的模型能做出来吗?”
罗切斯特大学调和分析专家 Alex Iosevich 在接受半岛电视台采访时说,OpenAI 似乎真的攻克了这个猜想,这是“历史性的进展”。提出者 Sogge 正是他的博士导师,这对他来说有着强烈的私人情感。他坦言自己一开始感到震惊,随后充满喜悦,但同时也承认心里夹杂着“一丝伤感”。这是面对机器推平人类几十年心智壁垒时,数学家最真实的本能反应。
然而回到验证维度,这份成果目前的处境有些尴尬。OpenAI 表示模型在 10 月 18 日生成证明,次日用 Lean 形式化了 6 个核心定理,论文和代码也都扔上了 GitHub。但这篇手稿是“直接放出”的,没有指定任何一个像 Williams 那样的学术复核小组。
直接放出来就万无一失了吗?看看前例就知道并非如此。10 月 6 日,OpenAI 曾一口气上传了七百多篇数学手稿。仅仅一天之后,仓库更新日志就显示,有 3 篇手稿因为一个“符号错误导致抵消论证失效”被直接撤回,另有 14 篇不得不做修补。仓库自身的说明文档也写得很坦白:未经过 Lean 形式化的结果“可能有问题”。
哪怕通过了 Lean 检查,也不能高枕无忧。今年 10 月,剑桥大学与伦敦国王学院的三位学者 Alexander Bastounis、Fabian Circelli 和 Anders Hansen 针对 OpenAI 之前宣称证明的纳维-斯托克斯方程爆破问题发了一篇预印本,标题就叫《Navier-Stokes lost in translation:为什么 Lean 验证 AI 自动形式化,不能保证自然语言证明正确》。学者们指出了自然语言论文与机器代码之间至少两处脱节。学者们并没有断言 OpenAI 的结论错了,而是证明了一个现实:机器检查通过了形式化代码,并不能推导给人读的论文就是严谨自洽的。同行评审依旧不可替代。
正如 MIT 数学家 Andrew Sutherland 所言:“我们应该要收据。”卷子已经摆在桌上,但谁来当判卷人、谁有精力把数千行的推导吃透,学界还没人正式接单。
杨-米尔斯与 QCD:锁在抽屉里的卷子
第三张卷子最神秘,也引发了最直接的学术冲突。
OpenAI 宣称,模型给出了四维时空下某些相互作用量子场论的严格数学存在性证明,其中包括描述夸克和胶子强相互作用的量子色动力学(QCD),以及纯杨-米尔斯理论。
首先必须澄清概念:克雷数学研究所设立的千禧年大奖难题中,“杨-米尔斯存在性与质量间隙”包含两个部分——严格证明理论存在,以及证明存在质量间隙(也就是粒子质量为什么不为零)。OpenAI 这次碰的只是“存在性”,并没有解决质量间隙,OpenAI 自己也没有宣称拿下了千禧年难题。在物理学家眼里,QCD 的物理有效性早已被实验验证了几十年;但在数学家眼里,其四维严格数学基础一直是未解之谜。
然而,外界现在根本无法评判这项成果的成色。因为这份材料目前四层里一层都没对外开放。论文没公开,代码没公开,题面没法核对,更谈不上全共同体的独立复核。
OpenAI 采取了所谓的“同行领航员(shepherds)”模式:他们把未公开的 AI 原始产出交给了诺贝尔物理学奖得主 David Gross 牵头的五人物理学家团队(还包括 Michael Douglas、Arthur Jaffe、Igor Klebanov 和 Nikita Nekrasov)。这个团队决定先不公开 AI 的原始材料,等他们自己理解吸收并写出物理学解读之后再公开发布。OpenAI 自己在公告里也承认,先挑选少数几个人“造成了信息不对称”。
这迅速在学界引发了强烈反弹。由普林斯顿高等研究院托管的“数学与人工智能顾问组”(AGMAI,成员包括菲尔兹奖得主 Timothy Gowers、Martin Hairer,物理学与数学巨擘 Edward Witten 等人)在 10 月 25 日专门发表声明,旗帜鲜明地反对 AI 公司“指定特权学者闭门审阅材料”。
AGMAI 列出了几条非常尖锐的理由:别人呕心沥血研究了几十年的课题,被指定的少数人却能拿着 AI 的底稿提前抢跑;挑选这些学者的过程完全不透明、无法问责;更关键的是,大牌学者的名字客观上成了 AI 公司的声誉盾牌,帮商业机构挡掉了本应面对的学术审视。
紧接着在 10 月 26 日,AGMAI 再次发布公开建议,点名要求 OpenAI 立即公开杨-米尔斯的自然语言证明和 Lean 代码。AGMAI 指出:既然 OpenAI 自己声称 Lean 形式化早在 10 月中旬就已经搞定了,那么延期公开的任何“科学理由”便不复存在。
这场争论的焦点已经不在于 AI 究竟算得对不对,而在于科学知识究竟应当如何在阳光下流转。
谁来买单?谁拿功劳?
当这三张卷子摆在一起,一个更现实的结构性矛盾暴露在所有人面前:功劳怎么分,账单谁来结?
OpenAI 在这方面表现得很慷慨,公开宣布不为这些发现寻求论文署名,把全部学术荣誉让给撰写解读和复核的学者,并且向 Simons 基金会捐赠了 500 万美元,用于资助学术界召开研讨会来消化 AI 产出的成果。
但学术界对此并不完全买账。在 Hacker News 的讨论中,有研究者一针见血地指出:500 万美元可能只够资助几个博士生读完几年,但现在的情况是,AI 公司靠着几乎无限的计算资源,几小时就能吐出成百上千篇高深手稿,然后把沉重繁琐的“质检工作”直接扔给全人类学术界做无偿劳动。
复核 ETH 的三位学者在公开信中表达了深深的忧虑:当 AI 能率先抛出答案时,荣誉和名声会不会只流向那些拥有最强算力工具、或者抢先把它发表出来的人?而那些花费数月甚至数年时间坐冷板凳、做艰苦核对和概念解释的人,他们的劳动又该如何衡量?早在今年 6 月,国际数学联盟背书的《莱顿宣言》就提出过类似的警示。
在科研的世界里,用暴力搜索或者启发式生成一个看似可行的复杂推导,成本正在急剧下降;而读懂推导、排除漏洞、确认本质概念的成本,不仅没有下降,反而在被指数级放大的信息垃圾所挤压。出题变便宜了,批改却越来越贵。
先看批改到第几层
回到那场热闹的发布会。在 Brockman 宣布推翻三大科学问题的推文发出一小时后,他发了那条简短的推特:“p still probably doesn't equal np”。
这耐人寻味的一句话,恰恰点出了所有严肃科研工作者面对这些大新闻时该有的定力:哪怕 ETH 的反驳完全成立,也不等于解决了 P vs NP;哪怕杨-米尔斯给出了存在性,也不等于拿到了千禧年大奖;哪怕代码在 Lean 里面跑通了,也不等于人类真正掌握了背后的规律。
AI 辅助科研的大门毫无疑问已经推开了。但它正在从“AI 到底能不能做出新东西”的初级猎奇阶段,进入“学术共同体到底能不能复核、怎样消化它”的制度博弈阶段。
以后再在朋友圈或热搜上看到“AI 证明了某某百年猜想”的轰动标题时,别急着感叹奇迹,不妨掏出这四把尺子量一量:
1. 完整的证明手稿能随时下载吗? 2. 它通过机器内核的严格逻辑检查了吗? 3. 机器跑的那个形式化题目,跟人类争论了一百年的猜想,是不是同一回事? 4. 有没有不拿钱、不签保密协议、愿意公开声明“参与不代表背书”的真正专家,坐在书桌前把它完完整整地读懂了?
在这些问题有清晰答案之前,卷子依然只是一堆未经验证的草稿。看懂了批改走到第几层,你才算真正看懂了这场科学变局。
参考
• Greg Brockman,X,宣布数学、理论计算机与物理三项科学发现 • Greg Brockman,X,关于推翻 ETH 后 P 大概率依然不等于 NP 的澄清帖子 • OpenAI,GitHub 开源仓库 openai/math,手稿目录与更新日志(history.md) • OpenAI,GitHub 开源仓库 openai/math,ETH 的 Lean 形式化文件 SubexponentialSAT.lean 与局部光滑配置文件 LocalSmoothing.json • Russell Impagliazzo、Ramamohan Paturi、Ryan Williams,公开信,关于独立审查 OpenAI 推翻 ETH 声称的原则声明 • Lean FRO,GitHub 开源仓库 leanprover/comparator,Comparator 证明评判工具文档 • Alexander Bastounis、Fabian Circelli、Anders C. Hansen,arXiv,论文《Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs》 • Advisory Group on Mathematics and Artificial Intelligence(AGMAI),官方网站声明,关于反对 AI 公司指定数学家接收成果的建议 • Advisory Group on Mathematics and Artificial Intelligence(AGMAI),官方网站声明,关于呼吁立即公开杨-米尔斯 AI 成果的建议 • Alex Iosevich、John Power,Al Jazeera,关于调和分析局部光滑猜想突破及学界反应的报道 • Ana Maria Constantin,The Next Web,关于 OpenAI 宣布推翻 ETH 及物理数学成果的报道 • Aamir Khollam,Interesting Engineering,关于 OpenAI 宣称在数学、计算与量子物理取得突破的报道 • Hacker News 讨论帖,关于 OpenAI 发布三项科学发现及推翻 ETH 论文的讨论(item 50251344)















































































