导语:OpenAI 周二在 GitHub 发布 722 篇数学手稿,称这些手稿全部由其尚未公开的内部模型生成。OpenAI 发言人表示,几乎所有内容来自交给单一 AI 代理的一条提示,部分输出可能经过多次尝试。若该说法成立,将对数学产生潜在重大影响,但学术界已要求提供可复现证据。

质疑与要求:麻省理工学院数学家 Andrew Sutherland 对 Scientific American 表示:“除非并直到他们发布模型,且人们能够复现结果,我认为任何关于单一代理一次性解决问题的说法都应被视为未经验证。”他补充说:“我们应当要求看凭证。”
数量口径:这些论文被归入 372 个相关结果“家族”。一个家族可以包含主定理、伴随论证、推论或替代证明,因此 722 是手稿数量,而非已解决问题数量。OpenAI 表示,其向模型提出约 4000 个问题,并保留其认为足够重要、值得发表的输出。平均每项结果约消耗相当于 ChatGPT Pro 三小时思考算力。这与上个月的 Navier-Stokes 声称形成对比,后者涉及 10000 个协调代理、工作 88 小时。
验证缺口:OpenAI 发布了其中 10 项结果的简化推理摘要。仓库中的形式化目录显示,722 篇论文中仅 162 篇带有计算机检查的主结果,约占 22%,并被翻译成 Lean;该软件可机械检查每一步逻辑。OpenAI 自己表示,并非所有手稿都有 Lean 形式化,而且“一些未形式化结果可能有问题”。换言之,许多已发布内容可能是错的。Lean 检查通过只能确认证明符合 Lean 中所写陈述,不能确认陈述与原问题匹配,也不能确认结果新颖或重要——这些仍需数学家判断。
学界反应:普林斯顿高等研究院在声明中表示:“现在的情况是,AI 可以在提示者无法理解、验证或对论证负责的情况下输出数学论证。我们认为,人类对数学的理解仍然至关重要。在这个新时代,我们如何努力实现一种新范式,将人类对数学的理解纳入负责任的学术输出?”也有人更兴奋。Abhishek Saha 教授称这是“数学的重要日子”,但指出大多数问题属于“现有项目中的例外进展”或“令人惊讶的突破”。大多数问题有趣,但并非不可能或像千禧年难题那样改变游戏规则。722 个问题中,只有一个被保留在该位置:准黎曼假设(Quasi-Riemann Hypothesis)。
发布透明度:此次发布也未达到高等研究院顾问小组 9 月 29 日建议的标准:模型名称、提示、思维链摘要、每个结果耗时与算力成本。OpenAI 发布了平均算力数据和 10 份推理摘要,但未发布提示,并表示仍在努力负责任地发布模型。多伦多大学数学家 Daniel Litt 持相反观点,认为没有理由要求公司对这些数学问题答案保密。Anthropic 上个月对经 Lean 检查的费马大定理证明采取不同路线,在 GitHub 公开发布全部 1300 万行。该证明形式化了 Andrew Wiles 1995 年发表的定理,而非声称新结果。OpenAI 表示将在获得 Lean 形式化后添加;目前 722 篇手稿中有 162 篇有。
