简述
- OpenAI 在 GitHub 上发布了来自一个未发布内部模型的 722 篇数学手稿，分为 372 个结果族。
- 722 篇论文中只有 162 篇带有 Lean 形式化的主要结果；OpenAI 也提醒，部分未经形式化的结果可能存在问题。
- 麻省理工学院的 Andrew Sutherland 表示，在该模型发布之前，“单提示、单代理”的说法仍未得到验证；此次发布也没有包含普林斯顿高等研究院顾问小组建议公开的提示词。

OpenAI 周二在 GitHub 上发布了 722 篇数学手稿，全部由其尚未发布的内部模型生成。OpenAI 的一位发言人称，几乎全部内容来自交给单个 AI 代理的一条提示；不过有些结果可能经过多次尝试。

这是一个大胆的说法，也可能成为数学领域一项意义重大的突破。但并非所有人都买账，也不是所有人都相信这种炒作。

麻省理工学院数学家 Andrew Sutherland 对《科学美国人》表示：“除非他们发布模型，并且人们能够复现其结果，否则我认为你应该把任何关于单一代理一次性解决问题的说法视为未经证实。”他说：“我们应该要求拿出实证。”

这些论文被分为 372 个相关结果“族”，一个结果族可以包含一个主定理以及配套论证、推论或替代证明。因此 722 是手稿数量，而不是已解决问题的数量。OpenAI 表示，它向模型提出了大约 4,000 个问题，并保留了它认为足够重要、可以发表的结果。

据 OpenAI 称，每个结果平均使用了大约相当于 ChatGPT Pro 思考模式三小时的计算量。而上个月有关纳维-斯托克斯问题的说法则大不相同：10,000 个协作代理工作了 88 小时。

OpenAI 为其中 10 个结果发布了简化的推理摘要。不过，根据仓库中的形式化目录，722 篇论文中只有 162 篇带有经计算机核查的主要结果。这大约是全部成果的 22%，已转化为 Lean——一种逐条机械检查每个逻辑步骤的软件。

OpenAI 自己也表示，并非所有手稿都有 Lean 形式化，而且“一些未经形式化的结果可能存在问题”。换句话说，他们发布的内容中可能有不少是错误的。

通过 Lean 检查只能确认证明确实是从 Lean 中写成的陈述出发推导出来的。它并不能表明该陈述与原始问题一致，也不能表明该结果是新的或重要的——而这一部分正是数学家现在必须评判的内容。

研究者们正是在这里皱起了眉头。

“我试图阅读 OpenAI 关于平面色数 >= 6 的证明。但这完全是令人难以置信的外星数学？不知何故，模型发现任何 K-着色 <=> “弱可测” K-着色，这似乎毫无来由。1/2 pic.twitter.com/W13ScT3nel”
—— Dmitry Rybin（@DmitryRybin1），2026年10月7日

“openai/math 仓库关闭了 Issues，也从未接受过拉取请求。这令人失望。如果你发布 722 篇手稿并请人们提供 Lean 形式化，你需要一个让人们提交的地方。”
“我正在用 Lean 4 形式化 OpenAI 的 Saxl 猜想证明，对照……”
—— Keith Adler（@keithadler），2026年10月7日

位于新泽西州普林斯顿的高等研究院在一份声明中表示：“现在的情况是，AI 可以在发出提示的人类无法理解、验证或为其负责的情况下输出数学论证。我们认为，人类对数学的理解仍然至关重要。在这个新时代，我们如何才能建立一种新范式，将人类对数学的理解作为负责任学术产出的一部分？”

不过，其他人则相当兴奋，例如 Abhishek Saha 教授。他写道：“这对数学来说是非常重要的一天”，但也指出，大多数问题属于“现有研究计划中的突出进展”或“出人意料的突破”这两类。

这意味着这批问题中大多数是有趣的，但并不是不可能解决或像千禧年问题那样改变游戏规则的问题。这样的地位留给 722 个问题中唯一的一个：拟黎曼假设（Quasi-Riemann Hypothesis）。

“关于 OpenAI 今天发布的 372 个结果（共 722 篇手稿），我还有一些进一步的想法。如果我要按开创性来对数学家证明并发表的理论进行分类，我（大致）会把它们分为四类：A）非突破性…… https://t.co/BA10SxBlx7”
—— Abhishek Saha（@ObhishekSaha），2026年10月7日

这次发布也没有达到高等研究院一个顾问小组在 9 月 29 日提出的建议：公布模型名称、提示词、思维链摘要，以及每个结果所花费的时间和计算成本。OpenAI 发布了平均计算数据和 10 份推理摘要，但没有发布提示词，并称仍在努力以负责任的方式发布该模型。

多伦多大学数学家 Daniel Litt 持相反观点，认为没有理由要求该公司将这些数学问题的答案保密。

上个月，Anthropic 采取了不同的路线，将其经 Lean 检查的费马大定理证明公开在 GitHub 上，全部 1300 万行。该证明形式化了 Andrew Wiles 在 1995 年发表的一个定理，而不是声称取得新结果。

OpenAI 表示，将在获得 Lean 形式化后继续添加；目前，722 篇手稿中有 162 篇带有形式化。