OpenAI宣布，其内部模型分别在调和分析、计算复杂性和量子场论中产出三项重大结果：证明所有维度上的局部平滑猜想，并由此推出Kakeya与Stein限制猜想；找到精确求解固定宽度SAT的次指数时间算法，从而否定广泛使用的指数时间假设（ETH）；以及给出四维杨–米尔斯理论、量子色动力学（QCD）和一类标准模型统一扩展的严格存在性证明。前两项已经公开自然语言论文和Lean形式化代码，第三项材料暂不公开，三项均尚未完成独立同行验证。真正值得关注的不只是结果本身，还有一种正在形成的新科研流程：AI快速生成证明，形式化系统检查推导，再由外部专家负责核验、解释和建立学术共识。
文章作者、来源：OpenAI
与其说是三项已确认突破，不如说是三份分量极重的“原始研究数据”
OpenAI在标题和X帖子中将这些工作称为“发现”，但在正文里采用了更谨慎的描述：目前的手稿最好被理解为“原始研究数据”，仍需要学术共同体将其转化为可以理解、复核和引用的科学知识。
三项成果的公开程度也不相同。调和分析结果已经直接公布；计算复杂性结果同时公开论文和Lean代码，并由外部专家组织验证；物理结果则只公布了结论与时间线，完整证明由专家小组暂时保管。OpenAI没有披露产出这些证明的具体模型名称、推理预算、搜索次数或失败样本。
从局部平滑出发，把Kakeya推广到所有维度
第一项结果属于调和分析。
局部平滑猜想研究波在传播过程中能够集中到什么程度。直观地说，即使某一瞬间的波可以高度聚集，把观察时间稍微平均之后，这种极端集中现象也应明显减弱。
该猜想之所以重要，是因为它与Kakeya猜想、Stein限制猜想等多个核心问题相连。2019年，Larry Guth、Hong Wang和Ruixiang Zhang解决了二维空间中的相应局部平滑问题；2025年，Hong Wang和Joshua Zahl证明了三维Kakeya猜想。
OpenAI现在声称，其模型借助一个新的辅助偏微分方程，证明了所有空间维度上的局部平滑猜想，并由此得到所有维度上的Kakeya结论和Stein限制估计。自然语言证明在10月18日产生，次日完成Lean形式化。
公开的Lean说明显示，形式化内容包括欧氏半波的局部平滑估计、Kakeya极大算子估计、Kakeya集合具有完整Hausdorff维数，以及若干Bochner–Riesz与球面限制估计。
这比单纯上传一篇AI生成论文更强，因为任何人都能下载代码，让Lean内核重新检查每一步推导。但这仍不等于数学界已经接受全部结论：专家还需确认形式化命题与传统猜想完全对应、定义没有被弱化，并检查自然语言论文是否真正解释了证明为何成立。
“ETH为假”不等于P等于NP
第二项结果对理论计算机科学的影响可能更直接。
指数时间假设认为，对于固定宽度的布尔可满足性问题，不存在随变量数量呈次指数增长的通用算法。过去几十年，大量图论、数据库、计算几何和计算生物学论文都把ETH作为条件，用来说明某些问题不太可能获得显著更快的算法。
OpenAI公开的论文给出一种确定性算法，可以精确计算固定宽度CNF公式的所有满足赋值。Lean形式化覆盖的运行时间为多项式因子乘以：
\(2^{O(n(\log\log n)^2/\sqrt{\log n})}\)
对于子句数量与变量数量成线性关系的情况，论文给出更强的：
\(2^{O(n/\sqrt{\log n})}\)
两者都是次指数时间，同时只需要多项式空间。
需要特别澄清：这并没有证明P等于NP。算法虽然比通常意义上的指数时间更快，仍然不是多项式时间；它推翻的是关于SAT究竟能快到什么程度的ETH，而不是直接解决P与NP问题。
这项结果由Russell Impagliazzo、Ramamohan Paturi和Ryan Williams牵头审查。前两人正是ETH最初的提出者之一。按照工作组要求，OpenAI公开全部原始材料，并承诺资助一次面向整个研究社区的会议。
物理结果最宏大，也是目前最无法核实的一项
第三项主张涉及四维量子场论。
OpenAI称，模型沿着建设性量子场论中的Balaban方法，给出了若干同时包含规范场与费米子的四维相互作用量子场论的严格存在性证明，其中包括QCD以及一种包含标准模型场与费米子的统一扩展。
这项工作还包含纯杨–米尔斯理论的存在性证明。纯杨–米尔斯理论是克雷数学研究所千禧年难题的一部分，但OpenAI的表述只涉及“存在性”这一子问题，不能据此称其已经完整解决包含质量间隙要求的千禧年难题，更不能称奖金已经产生归属。
模型据称在9月9日生成杨–米尔斯存在性证明，9月18日生成QCD证明，10月16日完成杨–米尔斯部分的Lean形式化。审查小组由诺贝尔物理学奖得主David Gross牵头，成员还包括Michael Douglas、Arthur Jaffe、Igor Klebanov和Nikita Nekrasov。
然而，论文和Lean代码目前都没有公开，外界只能核实OpenAI确实作出了这些声明，不能检查证明本身。因此，在三项结果中，这一项的不确定性最高。
Lean可以检查证明，却不能自动建立学术共识
Lean的作用，是确认一组明确定义的公理、定义和命题之间不存在未被系统发现的逻辑跳步。只要代码通过内核，它就提供了非常强的内部一致性证据。
但形式化验证仍留下两个重要问题。
首先，形式化命题是否完整对应学界原本讨论的猜想。如果翻译时改变了假设、作用范围或边界条件，Lean能够正确证明一个形式命题，却不能自动判断这个命题是不是人类真正关心的那个问题。
其次，一篇证明不仅需要正确，还要能够解释新方法为何有效、与既有文献有什么关系，以及能否推广。完成这些工作仍需要领域专家阅读、重构和写出可理解的版本。
因此，OpenAI提出了四项合作原则：不要求专家签署保密协议；不为内部模型生成的发现索取学术署名；专家应因核验、解释和扩展工作获得认可；参与自愿且无报酬，专家独立发表结论。
但这种制度仍有争议。OpenAI自己承认，指定首批“牧羊人”会造成信息不对称；其数学顾问组也警告，优先把未公开成果交给少数研究者，可能带来不平等访问、声誉借用和选择偏差。
科研瓶颈正在从“产生证明”转向“验证和理解证明”
如果这三项工作最终成立，它们的意义不只在于AI又解开了几个难题，而在于理论研究的速度结构可能发生变化。
模型可以在短时间内生成大量高度复杂的候选结果，Lean能够筛掉部分形式错误；随后最稀缺的资源会变成专家注意力——谁来确认问题定义、检查与既有文献的关系、解释新技巧，并判断结果是否值得继续发展。
这也意味着，“AI做出了发现”不应被理解为科学家已经退出流程。AI可能负责搜索和推导，形式化系统负责逻辑检查，而人类仍然负责问题选择、意义判断、学术信用和共同体认可。