简讯

OpenAI在GitHub上发布了722篇数学手稿，分属372个结果家族，全部出自一款尚未公开的内部模型。

OpenAI发言人表示，这些内容几乎全部来自一次交给单个AI代理的提示词，不过其中一些可能经历了多次尝试。

这是一项大胆的说法，也可能是数学领域的一项重要突破。但并不是所有人都买账。

“除非他们公开模型并且人们能够复现结果，否则我认为任何关于用单个代理一次性解决问题的说法都应视为未经证实，”MIT数学家Andrew Sutherland对《科学美国人》表示。“我们应该要求拿出证据，”他说。

OpenAI发布了其中10个结果的简版推理摘要。与此同时，根据仓库中的形式化目录，这722篇论文里只有162篇带有经过计算机检查的主结果，大约占全部内容的22%。这些结果被翻译成Lean——一种会机械检查每一步逻辑推导的软件。

OpenAI自己也表示，并非所有手稿都有Lean形式化，并称“部分未形式化结果可能存在问题”。换句话说，他们发布的很多内容可能是错误的。

Lean检查通过，只能说明证明在Lean中按所写陈述成立，并不能证明该陈述与原始问题完全一致，也不能证明结果是新的或重要的，而这正是数学家现在必须判断的部分。

而这也是研究人员开始皱眉的地方。

“我试着阅读OpenAI关于平面色数大于等于6的证明，但这完全是难以置信的外星数学？模型居然找到了任何K着色与‘弱可测’K着色等价，这似乎凭空出现。”Dmitry Rybin在X上写道。

“openai/math仓库关闭了Issues，也从未接受过pull request。这很令人失望。如果你发布722篇手稿并要求Lean形式化，就需要一个地方让人们提交它们。我正在用Lean 4形式化OpenAI关于Saxl猜想的证明……”Keith Adler在X上写道。

“如今的情况是，AI可以在提出问题的人类无法理解、无法验证、也无法为之负责的情况下输出数学论证，”普林斯顿高等研究院在一份声明中表示。“我们认为，人类对数学的理解仍然至关重要。在这个新时代，我们如何努力形成一种新的范式，把人类对数学的理解纳入负责任的学术成果之中？”

不过，也有人持更乐观态度。多伦多大学教授Abhishek Saha写道：“今天对数学来说是非常重要的一天。”但他指出，这些问题大多属于“现有研究计划中的非凡进展”或“令人惊讶的突破”。

这意味着，这组问题中的大多数都很有意思，但并不像千禧年难题那样不可能或具有改变格局的意义。722个问题中，只有一个属于那一类：准黎曼假设（Quasi-Riemann Hypothesis）。

“关于OpenAI今天发布的372个结果、涵盖722篇手稿，我还有一些进一步想法。如果我要按数学家证明并发表的定理的突破性来分类，我会非常粗略地分成四类：A）非突破性……”Abhishek Saha在X上写道。

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

Anthropic上个月对其经过Lean检查的费马大定理证明采取了不同做法，将全部1300万行公开发布到GitHub上。那份证明形式化的是Andrew Wiles在1995年发表的定理，而不是声称提出新的结果。

OpenAI表示，随着获得更多Lean形式化版本，公司会继续补充；目前，这722篇手稿中已有162篇带有Lean形式化。