一天上新722篇，一天撤回3篇

10月6日，OpenAI在GitHub上公开了一个代号为 openai/math 的仓库，一次性放入722篇数学手稿，归属于372个"结果家族"。据OpenAI称，这些结果来自一个尚未发布的内部前沿模型，针对约4000个未解决的数学问题生成，覆盖了从代数几何到理论计算机科学的广泛领域——其中包括对四维Kakeya猜想的解答、若干重要算法的改进，以及向黎曼猜想方向的进展。（来源：Scientific American，2026-10-06、The Verge）

OpenAI发言人向Scientific American表示：这批结果中几乎每一个，都是把单个提示词交给单个AI智能体一次性完成的，平均每个结果消耗约3小时的ChatGPT Pro级推理算力。作为对比，OpenAI此前9月宣布的Navier-Stokes奇点难题进展，动用的是上万规模的智能体集群、数百万美元级的算力。（来源：Scientific American）

如果这个说法成立，意味着强大的数学研究能力正在从"算力密集"走向"人人可及"——这本该是个令人兴奋的叙事。

然而10月7日，仓库的变更日志（changelog）出现了第一条撤回记录：三篇论文被撤下，十四篇被修订，另有十三篇更新了引用。从发布到第一轮撤回，间隔不到24小时。

一个正负号，如何压垮三篇论文

撤回通知写得异常简洁。问题出在《Algebraicity of Weil classes on split abelian eightfolds》这篇手稿：在一处关键论证中，论文把某个几何操作的符号写成了 +1，而按其自身约定应为 -1。

一正一负之差，后果是致命的。本应相互抵消归零的计数变成了非零值，而论文所依赖的经典定理恰恰要求这个计数为零。地基失效，后续构建全部悬空。

更麻烦的是依赖链。另外两篇论文——《Algebraicity of Kuga–Satake Correspondences for K3 Surfaces》和《The rational Hodge conjecture for products of K3 surfaces》——直接借用了这个构造，于是三篇一同撤回。这三篇都属于此前最受关注的Hodge猜想（千禧年七大难题之一）相关的结果家族，撤回后，该家族的名称也从"所有射影K3曲面的Hodge与Kuga–Satake结果"改成了"CM阿贝尔簇的有理Hodge猜想"——K3曲面部分被整体撤出了清单。（来源：KuCoin快讯、Cryptobriefing）

OpenAI在三份撤回通知中都强调了同一句话：撤回的是证明，不是命题本身——这些数学命题未必是错的，错的是论证过程。原稿未被删除，通过存档链接仍可访问，缺口说明写在明处。

有一处细节值得记录：变更日志末尾写着，"这使头条结果的形式化比例变为 300 / 719 ≈ 42%"。分母从722变成719是因为撤回，而那个分子，才是理解这场风波的钥匙。

42%的另一半：Lean绿勾能保证什么

Lean是一种证明助手语言，能逐行检验一个证明在逻辑上是否自洽。很多读者的第一反应是：这些不是机器验证过的吗？

答案是：截至撤回时，只有约42%的头条结果（300/719）附带Lean形式化证明。其余近六成没有经过任何机器检验，OpenAI自己的README也承认，"部分未形式化结果可能存在问题"。（来源：usecarly，2026-10-08、Ground Truth）

而且即便是那42%，Lean绿勾的保证范围也是有限的：它验证的是"给定形式化陈述，证明在逻辑上成立"，不保证形式化陈述忠实对应原命题，不保证结果是新的，更不保证人类能读懂它。Hacker News上有一个尖锐的评论版本：如果前提本身是错的，绿勾可以等价于一句 assert True。

这次被撤回或大幅修订的论文，有一个共同特征——几乎全部落在没有Lean形式化的部分。这反过来印证了数学界此前的提醒：未经形式化或同行评议的结果，目前只能算作"主张"（claims），不能算作"定理"。

验证的账单，以及账单面前的人

没有任何人否认这个模型做了真正的数学。争议从第一天起就不是"AI行不行"，而是两个更朴素的问题：谁来检查，以及来得及吗？

反应在48小时内迅速硬化。

数学家的职业组织直接发难。 数学人协会（Association for Human Mathematics）发表声明称，"数学家们没有要求这项工作被完成"，"一次发布700多个文件不是学术的展示，而是力量的展示"，并呼吁数学家"停止与OpenAI的合作"。（来源：usecarly）

菲尔兹奖得主陶哲轩发表了当天讨论最激烈的帖子《Math 2.0》，他的表述相对克制：这个领域"将需要淡化纯粹解题能力的角色，更整体地评价数学进步"，AI可以帮上忙，但这"比把最喜欢的AI智能体对准一批开放问题、然后等着要答案的'Math 1.0'心态，需要更多的想象力和雄心"。（来源：usecarly）

来自"震中"的体验最能说明问题。 斯科特·阿伦森在《The Mathocalypse》中转述了其合作者Dana Moshkovitz的经历：她花整个职业生涯追逐的Unique Games猜想，机器给出了一份证明——读起来"像某个用了致幻剂的人写出来的东西"，没有AI辅助基本无法阅读，引用常常不相关，构造"不是长码，不是短码——是某种外星式的古怪东西"。（来源：Professor Claw晨间简报，2026-10-08）

要求"看发票"的声音同样明确。 MIT数学家安德鲁·萨瑟兰的表态被广泛引用："在他们发布模型、人们能够复现结果之前，我认为应该把任何关于单个智能体一次性命题的主张都视为未经验证。我们需要看到receipts。"（来源：Scientific American、Engadget）

建议清单与实际做法之间的差距

这场争论有一个很少被注意、但极其重要的背景：OpenAI并非没有合规动作。9月21日，在首批10个结果引发震动之后，公司宣布组建了一个由数学家组成的独立顾问组，负责制定AI生成结果的负责任发布规范。顾问组给出的建议相当具体：把结果存入AI公司无法控制的学术仓储、附加持久可引用的标识符、公开模型名称、精确提示词、每个结果的推理摘要、耗时与算力成本，并尽可能提供形式化证明。

对照10月6日的实际发布，差距一目了然：

  • 仓储托管在OpenAI自己的GitHub账号下，而非独立学术档案库；
  • 模型未命名、未发布，外界无法复现任何结果；
  • 722篇中只有10篇附带推理摘要；
  • 单个问题的精确提示词与算力数据未公开；
  • 形式化覆盖约42%，是清单里落实得最扎实的一项。（来源：Tech-Insider、Implicator.ai）

一位评论者指出了其中的讽刺：顾问组的第一条建议本来就是——前沿实验室应当停止用专有模型测试高等数学。而这份722篇的发布，正是这一建议的反面。

写作很便宜，检查很贵

把整件事抽象出来，得到的是一个所有AI从业者都不陌生的结构：生产端的边际成本趋近于零，验证端的成本没有变。

生成一个证明，平均3小时推理算力；检验一个证明，需要稀缺领域专家数周的阅读，外加形式化专家把论证翻译成Lean。有研究者审计了OpenAI 8月首批10个结果：计算机检验的证明约20.6 MB，而人类必须阅读的形式化陈述只有55.6 KB——却引入了218个自定义定义而非领域共享的标准定义。他们的结论是：让检查"免费"，实际上只是把负担转移到了依赖稀缺专家注意力的层次上。（来源：Watts Up Next）

节奏的不对称加剧了问题。机器可以按机器的速度生产和更正，而必须理解这些结果的人类，正以人类的速度、多半无偿地、在一段机器不为他们优化的文本上工作。MIT的多尔·明策尔把这种处境称为"新闻稿式的数学"（math by press release）——据同行转述，他自己的团队为避免被OpenAI可能的发布"抢发"，曾在三天内赶出一篇95页的论文。（来源：byteiota）

这件事与每个技术人有什么关系

如果你不研究代数几何，这场风波依然值得放进你的技术判断里，理由有三。

第一，验证瓶颈是通用的，不是数学独有的。 今天AI生成的代码、报告、数据流水线，同样面临"写得快、验得慢"的困境。OpenAI的数学仓库提供了一个难得的公开样本：722篇里一天暴露出一个符号错误和一条三篇论文的依赖链。你自己的代码库里，AI生成部分的"Lean形式化率"是多少？

第二，发布节奏本身就是产品质量的一部分。 24小时撤回三篇、公开变更日志、保留原稿并标注缺口——就科学记录的规范而言，这套"追踪修改"的做法反而是整场风波里信用度最高的产物。问题不在于犯错，而在于用发布速度制造既成事实的压力。

第三，形式化方法正在从学术品味变成基础设施。 当机器能以小时为单位产出证明，Lean这类可机器检验的规范就不再是可选项。这对软件工程是同一个道理：当AI能以秒为单位产出代码，类型检查、测试、形式化验证这些"机器可读的正确性"，价值只会上升。

722篇论文的最终命运还没有定论——哪些结果经得起检验，需要几个月。但那个正负号已经提前说明了一切：机器负责证明的时代可能正在到来，而负责验证的，暂时还是人。

参考来源：