陶哲轩质疑 OpenAI：719 篇 AI 数学证明，人类真的理解了吗？

lymm2003

IT之家 10 月 9 日消息，OpenAI 于 10 月公布 719 份 AI 数学解答，涵盖 372 个数学结果族，涉及数百项开放研究问题，不过发布后被指尚未完全达到“数学与人工智能顾问小组”（AGMAI）提出的标准。
IT之家此前报道，OpenAI 于 10 月 6 日最初在 GitHub 发布 722 份 AI 生成数学手稿总数，涉及 372 个结果族及多项开放研究问题。不过于 10 月 7 日因一处符号错误及其连锁影响撤回 3 份，现公开目录为 719 份。
OpenAI 表示，发布前曾咨询普林斯顿高等研究院主持的“数学与人工智能顾问小组”（AGMAI），并参考其公开建议。然而，从公开信息看，此次发布尚未完全达到该小组提出的标准。
AGMAI 此前建议前沿 AI 实验室停止在专有、外界无法访问的模型上测试高难度数学问题，并要求披露模型名称、提示词、推理链、耗时及计算成本等信息；但 OpenAI 此次仍使用专有模型，且仅 10 份手稿附有模型推理链。
在人类可理解性方面，顾问小组强调 AI 生成证明应便于数学家审查和学习；但据报道，OpenAI 发布的证明中约 42% 未经形式化处理，也未提供将自然语言证明与形式化产物关联的机器可读元数据。

AGMAI 同时声明，其咨询角色不构成对 OpenAI 获取或发布这些结果的认可，最终仍需由数学界评估相关建议是否得到充分执行。该事件再度引发关于 AI 生成数学成果的透明度、形式化验证、同行审查及学术研究自主性的争议。
陶哲轩于 10 月 7 日在 mathstodon 上发布帖子，表示他并不反对 AI 做数学，甚至一直是 AI 辅助研究的积极使用者；但他强烈反对把“用 AI 快速攻克著名难题”当成主要目标或产品展示。他认为这会破坏数学共同体赖以运转的理解、教学、合作与开放探索机制。
陶哲轩指出，传统数学中，一个长期猜想的突破并不只是“得到答案”：作者会做报告、参加研讨、与同行交流，随后证明会被简化、解释、纳入教材，并催生后续问题、合作者和新的研究方向。
而 OpenAI 等公司当前的做法，往往是由提示者驱动 AI 自主解题；目标一旦“解决”，后续的理解、报告、同行讨论和领域建设却很少发生。陶哲轩认为，发布者甚至可能不足以解释 AI 的输出、回答问题或与领域互动。
他把这种状况称为数学界的“证明消化不良”：AI 能高速生成命题、证明和反例，但人类来不及验证、理解、写作、教学和吸收，结果出现大量“无人能消化的证明”。
他尤其担心的是，OpenAI 把纳维–斯托克斯方程等千禧年难题当作模型能力基准来攻克。在他看来，这把“解出多少题、多快解出”当成了衡量“理解与洞见”的指标；但速度和数量本身并不等于数学理解。
陶哲轩强调，问题一旦被公开“解决”，就几乎无法恢复为“未解决”状态。即使人们后来想寻找不同路径、从中提炼新方法，仅仅知道答案存在，也会“污染”这一探索过程。
因此，他批评这是一种不可持续的大规模“收割”：把开放问题当作可批量消耗的资源，最终会让整个数学领域变得不如传统研究方式下那样肥沃。
IT之家注：陶哲轩是当代最负盛名的数学家之一、加州大学洛杉矶分校（UCLA）数学教授，也是 2006 年菲尔兹奖得主；常被称为“数学界的莫扎特”。

羽绒服

AI 把历史财富吃干抹净之后，就会产生大量垃圾污染，这是无法回避的问题。
归根到底就是资本的力量，在工业革命乃至更早，资本对科学和技术贡献是巨大的，现在么，都不装了

choker

科学夹杂利益冲突让人不爽，但是免不了。

星花

放心，OA马上就会公布7190个没有人类看得懂的问题，然后宣布已经通过ai解决了。

拘翼

科学家科学圈应该回到以人为本，这是个好机会以后别搞那种象牙塔研究了，西方宣扬科学精神说什么第一动力是好奇心，但这里面没有道德，没有责任，这只会使得科学发展走大弯路，相比起来国内的很多伟大科学家目的很多是为了老百姓过好日子国家强大，这里面富含道德和责任，这才是科学发展的正路，而不要再提被西方炒作的什么莫名其妙的所谓科学精神（指好奇心）了。什么破好奇心，又不是小孩子，只是一种低级的非理性的情绪反应而已，人类的科学该长大了。

棍机凹升龙

意思就是让OA自己先去屎里淘金一下，别拉了一大坨就急着向外公布自己拉了

harry3

【【硬核解读】OpenAI为何撤回3篇数学论文？一个正负号如何让Hodge猜想证明失效？】 https://www.bilibili.com/video/BV1Dfpp66EVj/

依旧低级错误做不对基础算数

harry3

主楼新闻是写反了吧，是只有42%形式化。
更新中还新增了 6 项 Lean 形式化和 5 项辅助结果补充。按 OpenAI 的口径，目前已有 300 篇手稿的主结果完成形式化，占全部 719 篇的约 42%。

没形式化发个寂寞呢

Tienx

在攻克了114514个数学问题后，OA宣布成立仙童小学，欢迎各位数学家前来攻读

枯风瘦雪

harry3 发表于 2026-10-9 12:24
【【硬核解读】OpenAI为何撤回3篇数学论文？一个正负号如何让Hodge猜想证明失效？】 https://www.bilibili. ...

这个我觉得就是ai在数学科研上的应用最危险的一部分，ai是很可能基于不正确的生成结果快速产生大量“已解决”宣称的，而这很容易导向“充分验证ai成果”才能充分发挥ai辅助数学科研的能力……
希望在被ai产出的ddos冲击下还能有足够的数学共同体来完成对这些成果的验证吧……

赛肯特布拉泽

这个行为感觉像是刚拿到Agent工具的新手开发者，几乎没看AI写的东西，也不管是否有bug，就迫不及待的向别人仓库提交了大量PR，默认别人会免费进行review

孤舟垂钓

话说数学推理方面怎么避免AI幻觉啊

alitonz

想象中，出现在小说里那种桥段，这时会有一个敌对公司也拿AI审对手的稿，每审出一个错误，对手的股价就下降一点

以前的赛博小说真的没有这种剧情

枯风瘦雪

孤舟垂钓 发表于 2026-10-9 13:47
话说数学推理方面怎么避免AI幻觉啊

一般是通过prompt规避加上多个agent交叉检查挑刺吧，但从原理上肯定不能完全避免的，这次撤回的不就是一篇搞错符号得到一个“定理”，然后ai迅速在这个错误定理基础上继续生成了吗？还是主要靠跟ai协同的人类数学家自己去筛选

hentai烧酒

举个例子，计算器可以轻易计算四则运算，教师不让小学生用计算器，因为用计算器不利于学生思考和学习，不利于锻炼大脑。
陶的一些想法大概和这个例子解决，以前就能够用计算机进行穷举破解，现在AI更强，解答的速度也更快，有些问题确实可以得到结果，但却不能获得优雅的证明过程。

harry3

枯风瘦雪 发表于 2026-10-9 13:23
这个我觉得就是ai在数学科研上的应用最危险的一部分，ai是很可能基于不正确的生成结果快速产生大量“已解 ...

还没到那步，主要是o\这overclaim惯犯公司文化很有问题，没形式化的垃圾发出来干什么

枯风瘦雪

harry3 发表于 2026-10-9 14:23
还没到那步，主要是o\这overclaim惯犯公司文化很有问题，没形式化的垃圾发出来干什么 ...

形式化的部分也还没充分验证lean和自然语言叙述的等价性，确实是overclaim过头了，明显对不上进步主义者们的踩头热情……

scroll

Navier–Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs

作者：Alexander Bastounis, Fabian Circelli, Anders C. Hansen

出处：arXiv:2610.08144，v1 2026-10-06（math.AP / cs.AI / math.LO）

链接：https://arxiv.org/abs/2610.08144


这篇文章我理解如下


AI把原始数学问题翻译成Lean陈述时可能误译，导致“Lean前”和“Lean后”不是同一个问题；


AI在补全证明时可能悄悄改动或弱化Lean陈述，导致最终Lean证明对应的问题，和最初要证的不是同一个。