OpenAI 10 月 26 日一次公布了三项由其 AI 模型产出的研究成果，分属理论计算机科学、调和分析和数学物理。分量最重的一项，是给出了指数时间假设（ETH）不成立的证明。公司没有说明用的是哪个模型，只称”OpenAI 的 AI 模型”，并表示三项成果都还需要学术界进一步独立确认。
ETH：数百篇论文的地基
指数时间假设讲的是布尔公式可满足性问题（3-SAT）的计算难度：粗略说，它断言这类问题无法在亚指数时间内解决。它比”P 不等于 NP”更强，也更好用，几十年来被当作默认前提，图论、计算生物学、数据库、计算几何里有数百篇论文的下界结论都建立在它之上。
按 OpenAI 公布的时间线，模型在 10 月 16 日生成了自然语言证明，第二天完成 Lean 形式化。参与合作的是加州大学圣迭戈分校的 Russell Impagliazzo、Ramamohan Paturi，以及麻省理工学院的 Ryan Williams。前两人正是 ETH 的提出者之一。
据披露，几位学者向 OpenAI 提了两项条件：公开全部原始数据；出资办一场学术会议，专门讨论这一结果对计算机科学的影响。OpenAI 都答应了。如果证明经得起推敲，那批以 ETH 为前提的论文要逐篇重新评估，哪些结论只是”条件失效”、哪些可以换别的假设救回来，是一项不小的工程。
挂谷猜想：中国学者熟悉的一条线
第二项成果是在所有维度上证明了局部光滑猜想，并由此推出所有维度的挂谷猜想和斯坦因限制猜想。这里起作用的是模型构造出的一个辅助偏微分方程。OpenAI 称在 10 月 18 日拿到证明，次日完成 Lean 形式化，自然语言版本和 Lean 文件都已放上 GitHub。
这条线中文读者不陌生。局部光滑猜想由 Christopher Sogge 在 1991 年提出；2019 年，Larry Guth、王虹和张睿翔证明了二维情形；2025 年，王虹与 Joshua Zahl 证明了三维挂谷猜想，当时被视为调和分析多年来最重要的进展之一。从三维一步跨到所有维度，跨度很大，外部数学家怎么评价，目前还看不到公开表态。
杨–米尔斯：只有专家审读
第三项是数学物理。研究从严格数学意义上证明，四维空间里某些同时包含规范场和费米子的相互作用量子场论确实存在，涵盖量子色动力学，并顺带处理了纯杨–米尔斯理论存在性的一个子问题。纯杨–米尔斯理论的存在性与质量间隙，是克雷研究所千禧年大奖难题之一。
方法沿用 Tadeusz Balaban 的构造性量子场论路线。因为标准模型不能直接推到任意短的距离尺度，证明针对的是包含标准模型规范场与费米子的最简单大统一理论。审读由诺贝尔奖得主 David Gross 牵头，Michael Douglas、Arthur Jaffe、Igor Klebanov、Nikita Nekrasov 参与。这一项没有做形式化验证。
从 5 月到 10 月
把 OpenAI 今年在数学上的几次发布串起来看，节奏在加快，对象也在变。5 月是一道八十年的 Erdős 问题；9 月是纳维–斯托克斯方程的光滑性问题，同样带 Lean 文件，但当时没有数学家完成独立核验；这一次换成了一个被大量下游工作依赖的计算复杂性假设，还第一次把假设的提出者本人拉进合作名单。
验证方式也有分化：两项数学成果给出了机器可检查的 Lean 证明，物理那一项只能靠人审。Lean 能保证推导没有漏洞，前提是形式化时对命题本身的表述没有走样。这一点，仍要等独立团队把文件逐行读过才能确认。
参考来源：OpenAI 研究公告、CocoLoop、IT之家；GitHub 公开的 Lean 形式化文件核验证明对象与验证方式。