3篇手稿在发布不到24小时内因一个符号被撤回。10月6日，OpenAI在GitHub上发布了700多份预印本，宣称其内部AI模型取得了重大数学成果；不到24小时后，该公司已因错误撤回其中三篇手稿。 撤稿原因相当具体：发布第2天，就有3篇论文因为一个正负号写错被撤回，更多的稿子，专家读了也不知所云。 这显然不是普通练习题：722篇手稿涉及372个成果组，其中甚至包括多道长期困扰数学家的著名开放难题，准黎曼猜想、四维挂谷猜想、唯一博弈猜想都在清单之内。东方财富网微博知乎
幻觉最顽固的形态，是把错误藏在“形状”里。大模型按概率逐词生成内容，训练奖励的是“看起来合理”，不是“确实正确”；一个正负号写反并不破坏证明的任何结构特征，成稿照样流畅、工整、读起来像模像样。所以，模型生成了一个自称有效的证明，与一个数学问题真的已经被解决，是两个不同的主张，前者并不自动蕴含后者。 最直接的受害者是圈内人：深耕唯一博弈猜想多年的理论计算机科学家达娜·莫什科维茨第一时间研读了对应论文，发现里面充斥着难以理解的构造、语焉不详的推理步骤以及让人摸不着头脑的文献引用。 另一篇转述里，这份论文被形容为“像吃了致幻剂的人写出来的东西”——混乱、逻辑跳跃、充满人类从未见过的诡异构造。知乎知乎36氪
机器能检查逻辑，但检查不了“它检查的是不是原问题”
为了托底，OpenAI同步公开了部分成果的Lean形式化证明：让计算机逐步校验推导是否符合形式推理规则，相当于一台极严格的逻辑拼写检查器。但防线没有覆盖整个战场——截至10月7日，仓库中保留719篇手稿，约42%的主要结论完成形式化验证，OpenAI也承认未完成形式化的证明可能存在漏洞，除了撤回的3篇，还有14篇仍在修订。 防线上游还有第二道缝隙：剑桥大学研究者发现，AI把自然语言证明自动翻译成Lean代码时意义可能发生偏移——通过机器验证的是代码，未必严格对应原始证明里真正的那个命题。DeepTech深科技知乎
生成已经工业化，验证仍然靠人一页一页读
分领域抽查更直观：属于帝国学院凯文·巴扎德研究的数论领域成果有30篇，他认为只有7篇质量突出，而只有1篇通过了Lean形式化验证。 生成与验证的能力差，正是这批手稿全部主张的处境：模型已经能批量输出“看起来成立”的证明，而“确实成立”仍然要等数学家逐篇消化。知乎
数学界的愤怒不是饭碗，而是“证明消化不良”
这不是OpenAI第一次因发布方式被质疑：8月公布的10项数学进展很快被指出存在论证缺陷和引用问题，9月的纳维-斯托克斯方程成果又牵出与纽约大学数学家的优先权争议。 这次彻底点燃争议的导火索是发布形态：陶哲轩在个人博客转载“人类数学协会”的声明，该组织呼吁全球数学家停止与OpenAI合作，声明称“一次性发布700多份文件，展示的不是学术研究，而是权力”。 陶哲轩把现状概括为“证明消化不良”：AI以工业化速度批量生产证明，但人类根本来不及验证、理解和吸收。DeepTech深科技东方财富网36氪
对用户来说，读“AI数学突破”类新闻的正确姿势是把主张拆成三层：模型产出了“证明形状”的文本，人类同行能读懂并核验，形式化验证通过且对应原问题——目前绝大多数AI数学新闻仍停在第一层。一个正负号的翻车，恰恰是幻觉在“对错最分明”的领域里留下的最清晰标本：模型能逐字复刻正确证明的形状，却无法替任何人省略“逐步确认它成立”这个动作。眼下这项能力的成本还在下降，平均每项成果消耗的算力约等于ChatGPT Pro深度推理3小时，而9月攻克纳维-斯托克斯方程时还需数百万美元和88小时。 验证端能否跟上已有现成的观察信号：早在8月，OpenAI曾邀请约40位数学家讨论成果发布规范，而数学界的诉求归结为一句话——谁主张证明，谁就要为证明的可核查性负责。知乎DeepTech深科技
