10月6日，OpenAI把722篇AI生成的数学论文一次性放上GitHub，约42%配上了能用机器核查的Lean正式证明。 第二天，3篇手稿被撤回：一份证明推进时需要某个特定值为零，却在加减号上写错，必要条件随之失效，这份手稿以及依赖它的另外两篇一并撤下。 这场风波其实回答不了“AI未来能不能独立发顶刊”，因为它展示的是另一件事：OpenAI从一开始就没打算在顶刊门口排队，而真正卡住AI的，也从不是写论文的能力，是学术系统对“有人负责、有人读得懂”的要求。微博IT时代网
这批手稿全部出自一个未发布的内部模型，覆盖372个成果家族，方向横跨数论、几何、代数与理论计算机科学。产出清单里有黎曼zeta函数新的零自由区域，有Kaplansky直接有限性猜想特征二情形的证明，还有一份175页的四维挂谷猜想证明稿；分量最重的是Hodge猜想——克雷数学研究所七个千禧年大奖难题之一，这次在CM阿贝尔簇这类重要对象上被证明。 平均解决一道高难度难题，消耗约3个小时的顶级模型算力。 这不是刷竞赛题——2025年AI拿IMO金牌，解的还是人类早已知道答案的问题；这次是直接对着数学家没解决的开放问题要新结果。知乎36氪
撤稿的细节，比撤稿的数字更值得看。OpenAI表示，相关错误是在内部审查中发现的，将尽快更正，若无法修正则会撤稿。 仓库里的论文像软件一样挂着版本号、留着撤回日志：同时修复了14篇，连带更新了13篇的引用，而“未形式化的结果可能存在问题”这句话，发布时就写在了README里。 这批成果从第一天起就没被当成“已完成”的论文，而是当成一个可回溯、可打补丁的在线工程——这正是它与“发表”这个词的旧含义分岔的地方。IT时代网知乎
但机器核查不等于全部安全。剑桥大学与伦敦国王学院的研究人员发现，验证纳维–斯托克斯方程解法的Lean代码，加入了比论文声明更强的条件：论文称某步计算在更少条件下即可成立，代码却只在附加约束下跑通。 这意味着“代码跑通”证明的是翻译后的命题，未必是论文声称的那件事；何况仓库里约58%的结果连形式化都没有，对错仍要人类数学家逐篇审。更尖锐的质疑指向宣传口径：刷屏的“准黎曼猜想”并不是黎曼猜想本身，实际是零点分布界线的推进，有数学研究者直言这是靠名词打舆论擦边球。 一位把整个学术生涯押在“唯一博弈猜想”上的学者，读完宣称该猜想已被证明的手稿后，给出的评价是像吃了致幻剂的人写的东西。IT时代网知乎36氪
数学界的集体反弹，比撤稿本身更能说明“顶刊之问”的处境。发布当天，美国数学家组织AHM（人类数学协会）发声明，说一口气放出七百多份不是学术能力的展示，是权力的展示，并号召数学家停止和OpenAI合作。 第二天，陶哲轩把这份声明转上了自己的博客。他此前反复警告的是“证明消化不良”：难题一旦被宣布解决就再也回不到未解决的状态，会污染其他研究路径；而普林斯顿高等研究院设立的数学与AI咨询小组，第一份报告就划过红线——前沿AI公司不应该在内部模型上擅自测试高深数学难题，这次照样被绕开了。 普通用户的观感则是两极：有人喊“今天可能真的是数学史上的一个分水岭”，高赞笔记里也在问——老师，AI昨晚又挂了722篇，读，一篇一篇读？微博36氪小红书
把镜头拉回顶刊。机器进入数学证明的每一步，都在逼学术规则改一次口径：1976年阿佩尔和哈肯借计算机算了一千多个小时证明四色定理，数学界吵的是没人能检验的计算算不算证明。 五十年后吵的换成了“没人读得懂的证明要不要算发表”。同行评审从来不只是查对错，它同时生产人类的理解——而这恰恰是AI现在两头都不占的位置：正确性还压在58%未形式化部分的后续检验上，理解力上，写证明的一方不给解释，读证明的一方被折磨得痛不欲生。图灵奖得主杨立昆则持相反判断，他认为数学正迎来新时代，形式证明大幅自动化之后，重点会转向发展新概念与新猜想：船的发明降低了游泳的重要性，却让我们发现新大陆。知乎36氪
所以“AI未来能不能独立发顶刊”，这个问题本身可能问早了。顶刊的机制决定了署名者必须能为论文的每一步辩护、接受质询并承担责任，而这次事件最硬的证据恰恰相反：AI连加减号都会算错，错误还会顺着依赖链成片传导——在“解释”和“负责”这两件事上，AI连入场资格都还没有。但AI成果成为被学术界承认的记录，这条路其实已经走出来了：GitHub版本号、机器可核查的Lean证明、留痕的撤回日志就挂在所有人面前。真正决定终局的，不是AI哪天能写出零错误的论文，而是三件事何时同时成立——形式化比例够高、出现经人类验证并公认的分量级结果、学术共同体肯为“AI产出”重写作者与评审规则。在此之前，顶刊不会因为AI写对了而让步：它等的不是一篇不会错的论文，而是一个能解释自己论文的作者。
