资料名称： OpenAI 公开仓库 openai/math 中的两份 AI 研究文稿及配套 Lean 证明——《Local smoothing for the Euclidean wave equation》（欧氏空间波方程的局部平滑，任意维度）与《The Exponential Time Hypothesis is False》（指数时间假设为假）

帖内资料： 局部平滑文稿 PDF（791 KB）、ETH 否证文稿 PDF（867 KB）、局部平滑 Lean 形式化文件 079.md、ETH 否证 Lean 形式化文件 378.md 的原始地址

时间覆盖： AI 输出分别产生于 2026 年 10 月 16 日（ETH）与 10 月 18 日（局部平滑），Lean 形式化分别完成于 10 月 17 日与 19 日；OpenAI 项目说明发布于 2026 年 10 月 26 日

许可与引用： OpenAI 将稿件定性为「原始研究数据」，声明不寻求学术署名；仓库页面未标注开源许可，引用时注明 OpenAI、openai/math 仓库与具体文件名

适用任务： 阅读 AI 生成的证明原文、逐行核对 Lean 形式化文件、跟踪外部专家团队的独立核验进展

2026 年 10 月 26 日，OpenAI 发布项目说明《Working with academic communities to build scientific understanding》，宣布其模型在数学、计算机科学、物理学三个方向产出了新结果，并把数学与计算机科学两项的原始稿件直接公开到 GitHub 仓库 openai/math。

官方把这些稿件称为「原始研究数据」（raw research data），而不是完成同行评议的论文：读者拿到的是 AI 的自然语言输出和对应的 Lean 形式化文件，可以自行阅读、核对和继续研究。

局部平滑猜想由 Sogge 于 1991 年提出，属于调和分析，描述波在聚焦时的行为——最极端的聚焦必然短暂，随机典型时刻的聚焦量总是远小于最坏情形时刻。它的推论包括 Kakeya 猜想和 Stein 限制性猜想。此前人类工作的里程碑是 2019 年 Guth、Wang、Zhang 证明二维空间情形，以及 2025 年 Wang 和 Zahl 证明三维 Kakeya 猜想。

OpenAI 的模型给出了任意维度下局部平滑猜想的证明，技术核心是一个新颖的辅助偏微分方程（auxiliary PDE）。AI 输出于 2026 年 10 月 18 日产生，次日在 Lean 中完成形式化。帖内给出两份原始文件：791 KB 的自然语言文稿 PDF，以及 Lean 证明 079.md，两者可以对照阅读。

指数时间假设（ETH）是关于布尔公式可满足性问题（SAT）计算复杂性的长期猜想，与 P vs. NP 问题深度相关，曾被数百篇论文用来推导图论、计算生物学、数据库、计算几何等方向的条件性困难结果。

OpenAI 的系统证明了 ETH 为假：自然语言否证于 2026 年 10 月 16 日产生，10 月 17 日完成 Lean 形式化。对应材料是 867 KB 的文稿 PDF 和 Lean 文件 378.md。官方同时说明，这一否证重新打开了「这些任务还能快多少」的问题，但把理论进展转化为实际算法改进仍需要大量后续研究。

计算机科学结果由三位外部专家组织团队跟进：Russell Impagliazzo 与 Ramamohan Paturi（均为 UC San Diego，与 Francis Zane 同为 ETH 的原始提出者）、Ryan Williams（MIT）。团队要求所有原始数据公开以便社区独立核验，OpenAI 承诺资助一场会议讨论该工作对整个领域的影响。

数学结果则采用直接公开 AI 输出、由研究者自由组织解释的方式。

OpenAI 对合作列出四项原则：合作公开、参与者不签保密协议，可自由讨论与分享中间成果；OpenAI 不寻求学术署名，邀请专家担任管理人不意味着该专家或其工作组是原始发现者；合作团队对其撰写的文稿与发展的理解获得认可，并负责恰当引用所依赖的研究；参与自愿且无报酬，成员不代表 OpenAI 发言，OpenAI 也不代表他们发言。

此外，OpenAI 此前宣布向 Simons 基金会捐赠 500 万美元，用于支持研究者独立检验、解释和拓展这类 AI 产出的结果。

本帖交付的是数学与计算机科学两项已公开材料。物理学方向（量子色动力学与标准模型完备化）的外部团队决定暂不公开 AI 产出材料、改为自行撰写论文，因此不在本帖范围内。两份 PDF 位于仓库 preprints 目录下以标题和日期命名的子目录中，Lean 文件位于 lean/docs 目录，打开地址即可在线阅读或下载原件。

两份 PDF 文稿和 Lean 文件的完整地址都在下面，回复本帖即可查看。