新闻宏观经济OpenAI 发布秘密模型生成的 722 份数学手稿,研究人员要求提供证据

OpenAI 发布秘密模型生成的 722 份数学手稿,研究人员要求提供证据

作者: Decrypt·

要点速览

  • •OpenAI 发布了 722 份由未公开内部模型生成的数学手稿,组织为 372 个结果族,据称主要通过向单个智能体给出的一个提示词完成。
  • •722 份手稿中目前仅有 162 份(约 22%)包含经计算机验证的 Lean 主结果,其余约 560 份尚无形式化验证。
  • •OpenAI 仅公布了 10 个结果的简略推理摘要,且未公布提示词,未达到高等研究院顾问小组 9 月 29 日提出的披露建议。
  • •MIT 数学家 Andrew Sutherland 表示,在模型发布且结果可被独立复现之前,“单次生成”的说法应被视为未经证实。
  • •Abhishek Saha 教授称此次发布是数学界的重大一天,但指出 Quasi-Riemann Hypothesis 是唯一达到千禧年问题级重要性的结果。
OpenAI 发布秘密模型生成的 722 份数学手稿,研究人员要求提供证据

OpenAI 发布了 722 份由一个未公开内部模型生成的数学手稿,并称这些成果主要来自一个“单提示词、单智能体”的流程。这些论文被组织为 372 个相关结果族,但数学家表示,在模型、提示词及其他证据公开之前,无法对这些声明做出完整评估。

此次发布正值各 AI 实验室日益将数学作为前沿模型推理能力的试金石之际,它也成为检验 AI 生成的研究应如何发布、验证与披露的一次早期测试。

一位 OpenAI 发言人表示,几乎所有成果都来自给单个 AI 智能体的一个提示词,尽管部分结果可能经过了多次尝试。该公司称,其向模型提出了约 4,000 个问题,并筛选出其认为足够重要、值得发布的输出。

MIT 数学家 Andrew Sutherland 告诉 Scientific American,对“单次生成”的说法应持谨慎态度。“除非他们发布模型并且人们能够复现其结果,否则我认为任何关于用单个智能体一次性解决问题的声明都应被视为未经证实,”Sutherland 说。“我们应该要求拿出证据。”

722 这个数字指的是手稿数量,而非已解决的问题数量。一个结果族可以包含一个主定理以及配套论证、推论或替代证明。OpenAI 表示,平均每个结果使用了相当于约三小时 ChatGPT Pro 思考算力。这与该公司上个月的 Navier-Stokes 声明截然不同,后者动用了 10,000 个协同智能体运行 88 小时。

OpenAI 公布了其中 10 个结果的简略推理摘要。然而,GitHub 仓库中的形式化目录显示,722 份手稿中目前仅有 162 份包含经计算机验证的主结果。这约占全部收藏的 22%,意味着该结果已被翻译为 Lean——一种可机械验证每个逻辑步骤的软件。Lean 已成为数学领域机器验证证明的事实标准,这也是约 560 份尚未形式化的手稿成为整个收藏最大悬而未决问题的原因。

OpenAI 承认并非所有手稿都有 Lean 形式化,并警告称“部分未形式化的结果可能存在问题”。Lean 验证通过只能确认证明符合 Lean 中所写陈述,并不能证明该陈述与原始问题相符,也不能证明结果是新的或重要的。这些问题仍需数学家的审查。

研究人员已经对这批材料及其发布方式提出了质疑。Dmitry Rybin 在 X 上写道:

I was trying to read the OpenAI proof that chromatic number of a plane is >= 6. But it is totally unbelievable alien math? Somehow the model found that any K-coloring <=> "weakly measurable" K-coloring, which seems out of nowhere 1/2 pic.twitter.com/W13ScT3nel — Dmitry Rybin (@DmitryRybin1) October 7, 2026

Keith Adler 在 X 上写道:

The openai/math repo has Issues turned off and has never accepted a pull request. That's disappointing. If you publish 722 manuscripts and ask for Lean formalisations, you need somewhere for people to send them. I'm formalising OpenAI's Saxl's Conjecture proof in Lean 4 against… — Keith Adler (@keithler) October 7, 2026

位于新泽西州普林斯顿的高等研究院也对 AI 生成的数学工作的影响提出了质疑。“现在的情况是,AI 可以输出数学论证,而提出提示词的人却无法理解、验证这些论证,也无法为其负责,”该研究院在一份声明中表示。“我们认为,人类对数学的理解仍然至关重要。在这个新时代,我们如何构建一种新的范式,将人类对数学的理解纳入负责任的学术成果之中?”

Abhishek Saha 教授则持更为积极的态度,他写道:“对数学而言,这是非常重大的一天。”他表示,大多数结果属于“现有研究计划中的杰出进展”和“令人惊讶的突破”等类别。据他评估,这批收藏中包含有趣的问题,但没有能与其他七道千禧年大奖问题——即克雷数学研究所各设 100 万美元奖金的题目——相媲美的结果。他指出,Quasi-Riemann Hypothesis(准黎曼假设)是 722 个结果中唯一达到那一重要级水平的题目。

Saha 在 X 上写道:

Some further thoughts on the 372 results released by OpenAI today, across 722 manuscripts. If I were to classify theorems that mathematicians prove and publish according to their groundbreaking nature, I would (very roughly) divide them into four categories: A) Non-breakthrough… — Abhishek Saha (@ObhishekSaha) October 7, 2026

此次发布也未达到高等研究院顾问小组于 9 月 29 日提出的建议。该小组建议披露模型名称、提示词、摘要化的思维链、每个结果所耗时间及计算成本。OpenAI 提供了平均计算数据及 10 份推理摘要,但没有公布提示词。该公司表示,仍在努力以负责任的方式发布该模型。

多伦多大学数学家 Daniel Litt 持相反立场,认为没有理由要求 OpenAI 对这些数学问题的答案保密。

Anthropic 上个月采取了不同的做法,将其经过 Lean 验证的费马大定理证明的全部 1300 万行代码公开在 GitHub 上。那项工作形式化的是 Andrew Wiles 于 1995 年发表的定理,并未提出新的数学结果。这两次发布凸显了业界在披露策略上的分歧:一边是对已知定理完整且经机器验证的证明,另一边是带有部分形式化验证的大批新声明。

OpenAI 表示,将在获得 Lean 形式化后陆续补充。目前,722 份手稿中有 162 份拥有形式化的主结果。其余手稿的地位如今取决于研究人员所说的他们最需要的东西:模型的发布、底层提示词,以及对剩余手稿的独立形式化验证。