AI一口气交出722篇数学论文，如今缺的是来读这些论文的数学家

2026年10月6日，OpenAI在官方博客发布了《Sharing AI progress in mathematics》，同时把一个尚未公开的内部模型写出的722篇数学手稿，一次性上传到自家的GitHub仓库。公开第二天，OpenAI撤回了其中3篇。同一天的变更记录写道，撤回后剩下的719篇手稿中，证明经Lean这一证明检查程序确认无误的约占42%。其余手稿对不对，只有靠数学家亲自阅读才能知道。 openai +2

OpenAI让AI模型解约4,000道数学研究问题，并把结果整理成722篇手稿一次性公开

根据仓库的README，大部分结果是用未公开的内部模型按同一流程得出的。评估期间，OpenAI给模型出了约4,000道研究问题，并把结果整理为372组。372是产出结果的问题数，一个结果可能对应多篇手稿，所以手稿总数达到722篇。关于筛选标准，README只写了一句，即要求具有“适当程度的重要性”。约4,000道题中有多少失败、372道具体如何挑选，README都没有写明。OpenAI表示，每个结果平均消耗的算力，大约相当于ChatGPT Pro思考3小时所用的算力。 github +1

OpenAI称这项工作是模型评估的一部分。现有的数学考试题，模型几乎都能解出，因此评估范围扩展到了尚无答案的研究问题。除手稿外，OpenAI还公开了部分Lean形式化、10份模型推理摘要、算力估算，以及尝试问题数量的统计。 github +1

并非所有结果都走了这套流程。README说明，黎曼ζ函数无零点区域的工作，以及CM阿贝尔簇霍奇猜想的证明，都是在这套流程之外得出的；Re(s) > 11/12无零点区域的手稿则经过改写，方便人阅读。这次发布同时也是OpenAI为一个尚未推出的模型所做的成果展示。博客写道，OpenAI打算“负责任地发布”（responsibly release）这个模型。 github +1

公开次日，OpenAI撤回了3篇证明中有计算错误的手稿，另外还修改了14篇手稿的证明

仓库变更记录（history.md）10月7日的条目同时列出了撤回3篇、证明修改14篇、仅修改引用13篇、新增形式化6项。Retraction Watch也报道称，撤回发生在公开次日。不过，撤回公告正文写的撤回日期是10月6日，与变更记录的日期相差一天。 github +2

撤回始于一篇题为《Algebraicity of Weil classes on split abelian eightfolds》的手稿。据撤回公告，这份证明在某一步计算中把符号记为+1，实际应为−1。就因为这一个符号写反，本应为0的值变成了非零值（−2m），证明所依赖的定理（Eliashberg–Murphy消失定理）因此不再适用。借用了这篇手稿构造的2篇K3曲面相关手稿也一并撤回。公告最后一句是：“此次撤回针对的是证明，并不意味着命题为假”。公告把证明出错和命题出错分开写明。 github +1

修改了证明的14篇，原因与这个符号错误不同。变更记录写道，这14篇是出于修补证明、修正表述等其他原因修改的。 github

至于是谁最先发现错误，能确认的只有OpenAI发言人对Retraction Watch说的，是在“审计（audit）过程中”发现的。研究负责人Dan Roberts在X上总结为“新增6项Lean形式化、19处修改、3篇撤回”（6 new Lean formalizations, 19 modifications, and 3 withdrawals）。这19处修改如何对应变更记录中的14篇证明修改和13篇引用修改，公开说明中没有交代。尽管如此，由于公司自己按日期留下了更正记录，外界也能追踪到底改了什么。 retractionwatch +1

剩下的719篇中，证明经程序验证的只有42%，其余58%要靠数学家亲自阅读确认

变更记录写着“300 / 719 = ~42%”，意思是撤回后剩下的719篇手稿中，有300篇的证明已用Lean形式化。Lean是这样一种工具：把证明改写成计算机能读的代码后，程序会检查每一步在逻辑上是否成立。这个42%是公开次日新增6项形式化之后的数字。公开首日的README只说形式化“很多，但不是全部”（Many, but not all），没有给出比例。 github +1

其余约58%没有经过机器验证。README自己也写道：“部分未形式化的结果可能存在问题”（Some of the unformalized results could have issues）。发言人对Retraction Watch说，“大约50%”的结果是在未经确认的情况下公开的，这与根据仓库数字算出的58%对不上。本文以仓库中的数字为准。 github +1

在形式化完成之前公开是否妥当，也存在分歧。发言人说，IAS的独立咨询小组AGMAI曾建议不必等到完全形式化再公开。AGMAI建议的第4条写道，如果形式化会造成不可接受的延迟，应明确说明形式化状态。但同一份建议在第一段就表示，不支持AI实验室用内部模型测试高等数学问题的做法，并建议把结果发布在AI实验室不控制的仓库中。OpenAI把手稿发在自家GitHub上，并在博客中写道正在考虑由社区运营的替代方案。Cornell的Alex Townsend说，OpenAI本应先发布经Lean验证的手稿，其余的另行发布，并请大家协助验证。 retractionwatch +2

对于Lean验证能否原样保证手稿中的证明，另一个案例中出现了质疑。Cambridge的Anders Hansen等3人指出，在OpenAI 9月通过另一个仓库发布的Navier-Stokes证明中，Lean代码证明的是一个与自然语言证明不同、更弱的命题。他们举例说，自然语言证明处理的是m+4阶导数，而Lean代码处理的是m+5阶导数。这篇论文分析的并不是此次的719篇。Hacker News上也有人反驳：把最终命题改写成Lean时所用的定义是人事先写好的，所以最终命题没有问题，出现偏差的只是中间步骤。争论仍在继续。不过，程序检查的对象是改写成Lean的命题。这个命题与手稿中的文字是否表达同一内容，最终仍要由人来确认。 arxiv

数学家们说，逐篇阅读核实这些手稿，负担大到得停下自己的研究

Hansen对New Scientist表示，“这些由大语言模型生成的证明都必须由人来阅读，这给数学家带来了巨大的额外负担”。 newscientist

集合论学者Asaf Karagila在个人博客的“问题清单”页面上承诺，谁解出划分原理（Partition Principle）问题，就送谁一瓶威士忌。Karagila称这个问题已有100多年历史。OpenAI宣布解出这个问题后，有人问Karagila会不会给Sam Altman寄威士忌。Karagila的回答是：“答案是不会”（The answer to that is no）。 karagila

“我正努力完成好几篇论文，还在指导几位博士生，自己手上也有大量研究。我什么时候去细读一篇写得很糟的论文？”（“I am trying to finish several papers, I am supervising a number of Ph.D. students, and I have a lot of active research of my own to do. When am I supposed to sift through a badly written paper?”）……“如果要认真对待，这就相当于一次拒绝服务攻击：放下其他一切，先把这个弄明白。”（“But it is the equivalent of a Denial of Service, should we want to take it seriously: stop everything else and figure this one out.”）（Asaf Karagila）

不过Karagila也说明，自己没有看过Lean代码。Karagila批评的是手稿的写作质量，并没有说证明是错的，还写道自己并不反对使用AI本身。 karagila

Terence Tao（UCLA）从数学共同体的角度看待同样的负担。过去，一个重要证明问世后，讲座、研讨会和合作往往接踵而来，许多数学家借此理解这个证明。Tao指出，用AI解题的人对结果理解不够，无法回答问题或做讲座，因此带动的研讨会和合作要少得多。 mathstodon.xyz

也有更强烈的反对声音。Association for Human Mathematics在10月7日的声明中说：“一次性发布700多个文件，展示的不是学术，而是权力”（Releasing over 700 files at once is not a demonstration of scholarship, but a demonstration of power），并呼吁数学家停止与OpenAI合作。MIT的Andrew Sutherland称迅速撤回是“负责任的做法”（the responsible thing to do），但也表示，要挽回失去的信任还需要做多得多的事。 ahmath +1

欢迎这次公开的人也承认负担很重。多伦多大学的Dan Litt对Fortune说，这“对数学来说是件大好事”（this is great for mathematics）。同时Litt表示，要从这些结果中获得理解，需要投入大量人力，只是这种劳动与数学家一直以来所做的并无太大不同。Litt还认为，OpenAI内部没有足够多、覆盖足够多领域的数学家来理解所有证明。 fortune

AI把结果成批倒出来之后，数学缺的东西正从生产证明的能力，转向阅读、核实证明并为之负责的人

这次公开的材料里缺了一个数字：一个人读完并核实一篇手稿需要多少时间。这个数字既不在OpenAI的材料里，也不在批评者的文章里。相比之下，生产证明一方的成本已经以数字公开：约4,000道题，每个结果平均相当于ChatGPT Pro思考3小时的算力。核实一方公开的数字只有经程序检查的300篇，其余419篇要等数学家抽出时间才能确认。 github +1

公开次日，3篇手稿被撤回，另有14篇手稿的证明被修改。Townsend认为还会发现更多错误。看到变更记录附有版本说明和撤回版本的存档链接，一位Hacker News用户写道：“软件工程的做法遇上数学，就是这个样子”（This is what it looks like when software engineering practices meet mathematics）。手稿先发出来，核实和修改在公开之后才跟上。 github +2

Tao提出的“Math 2.0”是对这一变化的一种回应。Tao认为，应当让解题退出数学的中心位置，更看重把结果讲清楚的阐释工作和建设共同体的工作。OpenAI也在博客中写道，今后会资助研讨会和学术会议。生产一个证明的成本已经以算力的形式公开，但阅读这个证明、找出错误并撤回、回答提问，仍然要靠每一位数学家用自己的时间来填补。 mathstodon.xyz +1

过去的数学最看重的，是解出难题、做出证明的能力。AI一口气交出722篇手稿后，产出的手稿有一半以上在等人阅读核实。如今数学该投入精力的，是阅读并核实证明、向其他数学家讲清楚，以及在发现错误时承担责任。

延伸阅读

openai/math 变更记录 OpenAI按日期记录的更正，列出撤回3篇、证明修改14篇、引用修改13篇，以及形式化比例300/719。 github.com

AGMAI建议：Responsible Release of AI-Generated Mathematics IAS咨询小组9月29日发布的建议，涉及用内部模型测试的做法、发布渠道和形式化状态的标注。 agmai.org

Terence Tao，Math 1.0 vs Math 2.0 Tao解释AI解出的结果为何没有带来讲座与合作，以及数学共同体应当更看重什么。 mathstodon.xyz