陶哲轩质疑 OpenAI：719 篇 AI 数学证明，人类真的理解了吗？
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 把历史财富吃干抹净之后，就会产生大量垃圾污染，这是无法回避的问题。
归根到底就是资本的力量，在工业革命乃至更早，资本对科学和技术贡献是巨大的，现在么，都不装了 科学夹杂利益冲突让人不爽，但是免不了。 放心，OA马上就会公布7190个没有人类看得懂的问题，然后宣布已经通过ai解决了。 本帖最后由 拘翼 于 2026-10-9 12:16 编辑
科学家科学圈应该回到以人为本，这是个好机会以后别搞那种象牙塔研究了，西方宣扬科学精神说什么第一动力是好奇心，但这里面没有道德，没有责任，这只会使得科学发展走大弯路，相比起来国内的很多伟大科学家目的很多是为了老百姓过好日子国家强大，这里面富含道德和责任，这才是科学发展的正路，而不要再提被西方炒作的什么莫名其妙的所谓科学精神（指好奇心）了。什么破好奇心，又不是小孩子，只是一种低级的非理性的情绪反应而已，人类的科学该长大了。 意思就是让OA自己先去屎里淘金一下，别拉了一大坨就急着向外公布自己拉了 【【硬核解读】OpenAI为何撤回3篇数学论文？一个正负号如何让Hodge猜想证明失效？】 https://www.bilibili.com/video/BV1Dfpp66EVj/
依旧低级错误做不对基础算数 主楼新闻是写反了吧，是只有42%形式化。
更新中还新增了 6 项 Lean 形式化和 5 项辅助结果补充。按 OpenAI 的口径，目前已有 300 篇手稿的主结果完成形式化，占全部 719 篇的约 42%。
没形式化发个寂寞呢 在攻克了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幻觉啊 想象中，出现在小说里那种桥段，这时会有一个敌对公司也拿AI审对手的稿，每审出一个错误，对手的股价就下降一点
以前的赛博小说真的没有这种剧情 孤舟垂钓 发表于 2026-10-9 13:47
话说数学推理方面怎么避免AI幻觉啊
一般是通过prompt规避加上多个agent交叉检查挑刺吧，但从原理上肯定不能完全避免的，这次撤回的不就是一篇搞错符号得到一个“定理”，然后ai迅速在这个错误定理基础上继续生成了吗？还是主要靠跟ai协同的人类数学家自己去筛选 举个例子，计算器可以轻易计算四则运算，教师不让小学生用计算器，因为用计算器不利于学生思考和学习，不利于锻炼大脑。
陶的一些想法大概和这个例子解决，以前就能够用计算机进行穷举破解，现在AI更强，解答的速度也更快，有些问题确实可以得到结果，但却不能获得优雅的证明过程。 枯风瘦雪 发表于 2026-10-9 13:23
这个我觉得就是ai在数学科研上的应用最危险的一部分，ai是很可能基于不正确的生成结果快速产生大量“已解 ...
还没到那步，主要是o\这overclaim惯犯公司文化很有问题，没形式化的垃圾发出来干什么 harry3 发表于 2026-10-9 14:23
还没到那步，主要是o\这overclaim惯犯公司文化很有问题，没形式化的垃圾发出来干什么 ...
形式化的部分也还没充分验证lean和自然语言叙述的等价性，确实是overclaim过头了，明显对不上进步主义者们的踩头热情…… 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证明对应的问题，和最初要证的不是同一个。 有些数学问题就没必要，可能也不可能被人类理解。
人类说到底就是一群猴子形状的肉团，但可能有些真理就是需要一千万步、甚至一亿步的证明，解答过程人类一辈子也读不完，理解不了很正常。
前几天是一个问题的答案太长，需要数学家花很长时间读答案整理归纳，现在是题目太多，需要很长时间读题目，但至少题是人出的。
以后计算机自己出题目，自己解答，人类可能连题目都读不懂。这也没办法 choker 发表于 2026-10-9 12:00
科学夹杂利益冲突让人不爽，但是免不了。
陶哲轩是最早最深入和AI头部玩家保持长期合作推动AI4Math的顶级数学家代表。
而和他合作的这个头部玩家叫做OpenAI 浪子龙飞z 发表于 2026-10-9 14:45
陶哲轩是最早最深入和AI头部玩家保持长期合作推动AI4Math的顶级数学家代表。
而和他合作的这个头部玩家叫 ...
也是推动lean在数学科研应用的头部数学家，不然现在ai大厂还没有那么容易claim这些结果…… hentai烧酒 发表于 2026-10-9 13:59
举个例子，计算器可以轻易计算四则运算，教师不让小学生用计算器，因为用计算器不利于学生思考和学习，不利 ...
应该不是这个意思，是拿出来的结果根本没人看得懂，等于github里的一堆vibe出来的没注释的代码 本帖最后由 枯风瘦雪 于 2026-10-9 15:13 编辑
说到对openAI的N-s爆破解方程的那个质疑文章，文章论点是自然语言版本和lean编译通过的版本不等价，作者倒也没到直接推翻的底部
所以说回来，openai的原始论文确实是需要同行好好review一下的，到底这个爆破是不是成立还是挺关键的，别搞得已经默认这个结果就正确了……
ai出的代码，至少可以跑一下看是不是想要的，ai画图出视频下棋反正输出的东西人可以看结果，但是ai用人类无法理解的方法解数学题，谁来认证这个解法对不对呢？ 话说围棋从阿法狗出现到现在总结出啥新定式了么？搞懂ai的下棋逻辑了嘛，还是就单纯死记硬背（事先声明我完全不懂围棋 陶哲轩一直以来的发言我觉得是没什么问题的，AI是手段，人才是目的。如果AI的产出无法帮助人更好的去了解和解决数学问题进而去解决更多的问题，那吐出来一堆证明、论文又有什么用处呢？ 之前的相对论，麦克斯韦方程，量子理论数学的贡献太大了。
所以大家默认数学是科学之母，即使目前没用的数学研究，也可能在将来某个时刻起到巨大的作用。有个说法就是无用之用。
其实功利的说，科学和数学都是要实用主义的，尤其是数学。
因为数学是形而上学，显然有无穷个问题，这无穷个问题去掉因为哥德尔不完备导致无法证明的，依然是无穷。
但是个人和人类的生命是有限的，要放在有价值有意义的事情和方向。 但 OpenAI 此次仍使用专有模型，且仅 10 份手稿附有模型推理链。
一般管这种行为叫造屎
—— 来自 HUAWEI CMM-AL10, Android 16, 鹅球 v4.0-alpha 关键是review AI做出的论文没法算科研绩效啊 本地部署qwen3.8flashnext nvfp4 strata。。。
速度很满足了 数学界会引来一次大洗牌，和围棋一样。现在围棋棋手的身份**变化了，不是某一项脑力竞技项目的智力巅峰，而是娱乐网红，成绩也没那么重要了，战鹰柯洁平分流量。
数学界会怎么样静观其变。
我作为个人虽然是智力渣渣，也是站人类一边，怀念古法旧时代，趋势不可阻挡。 heemoon 发表于 2026-10-9 15:44
话说围棋从阿法狗出现到现在总结出啥新定式了么？搞懂ai的下棋逻辑了嘛，还是就单纯死记硬背（事先声明我完 ...
目前的高手大概能在ai的启发下找到它对于棋盘整体价值判断的那种“感觉”，也算是某种意义上搞懂了一些？毕竟之前也是靠“厚薄”这种玄学感觉去做判断的
至于新定式，点33的定式都是ai兴起之后流行起来的啊 拘翼 发表于 2026-10-9 12:13
科学家科学圈应该回到以人为本，这是个好机会以后别搞那种象牙塔研究了，西方宣扬科学精神说什么第一动力是 ...
狗屁不通，还是你是真的在串？ icebluesky 发表于 2026-10-9 15:50
关键是review AI做出的论文没法算科研绩效啊
不review很快就要被ai slop挤压自己的科研绩效空间了，真的是两头挨打的 枯风瘦雪 发表于 2026-10-9 15:54
不review很快就要被ai slop挤压自己的科研绩效空间了，真的是两头挨打的
反正从科研管理角度来看目前ai对学术界的最大冲击是ai产物需要大量审稿人review但传统上review是个义务劳动导致原来的绩效管理模式快被击穿了。
至于成果到底是人出的还是ai出的，只要成果本身没问题，大家并没有那么在意。 icebluesky 发表于 2026-10-9 15:58
反正从科研管理角度来看目前ai对学术界的最大冲击是ai产物需要大量审稿人review但传统上review是个义务劳 ...
我说的绩效被挤占主要是，万一有人利用ai claim一个直接影响你成果价值的东西，就会很尴尬
比如这次被openai扫射的相关领域的研究者，他们不可能毫无保留地接受ai宣称的成果，又不能装着看不见这些claim继续古法科研，两头挨打的感觉还挺惨的 一会儿数学，一会物理，对这帮AI公司来说就一个目的：“我马上就要AGI了，继续投资，不要停” 这不就是开源社区被AI生产的PR挤爆的翻版么？
—— 来自 HUAWEI VYG-AL30, Android 12, 鹅球 v3.5.99 icebluesky 发表于 2026-10-9 15:58
反正从科研管理角度来看目前ai对学术界的最大冲击是ai产物需要大量审稿人review但传统上review是个义务劳 ...
现在好多peer review都是ai了 Re:Source 枯风瘦雪 发表于 2026-10-9 16:00
我说的绩效被挤占主要是，万一有人利用ai claim一个直接影响你成果价值的东西，就会很尴尬
比如这次被ope ...
是这样，他宣称自己解决了，那不管你信不信你都得验证要不然你的成果发不出来。
验证了最好结果是他是错的你还能继续做，但你花了大量时间给o÷打白工；最差结果是他对的，不光给o÷打白工还得换方向，输麻了。
页:
[1]
2