10月7日，OpenAI把内部前沿模型产出的722篇数学手稿一次性放上GitHub，归入372个成果族，没预告，也没走同行评审。第二天，仓库挂出第一份更新日志：撤回3篇，修订14篇，13篇更新了引用。手稿总数从722变成719。
撤稿原因简单到让人愣神——用36氪报道里的原话说："一个正负号写错了。"
前天我们刚写过OpenAI和数学界"按规矩交作业"的博弈，今天这件事算是给那场博弈补了一个最生动的注脚：规矩不是白立的，连最强的模型，也会在最基础的地方翻车。
一个符号，怎么就拖垮了三篇论文
被撤回的三篇手稿都指向千禧年大奖难题之一的霍奇猜想，属于仓库里最受关注的第032号成果族。
问题出在第一篇。OpenAI在撤稿说明里写得很直白：论文在一处关键论证中，把一类几何操作的符号记成了+1，而按论文自己的约定，它应当是-1。
一正一负，差之毫厘。原本应该相互抵消、最终归零的一个计数，变成了不为零的数。而论文所依赖的一个经典定理，前提条件恰恰是这个计数必须为零。前提塌了，整套构造随之失去支撑。另外两篇借用了这套构造，于是一并撤回。
值得注意的是OpenAI的处理方式：三份撤稿说明都强调同一句话——撤回的是证明，不意味着数学命题本身是错的。原稿也没删，归档链接仍可查看。032号成果族的名字随之从"所有射影K3曲面的霍奇与Kuga–Satake结果"改成了"CM阿贝尔簇的有理霍奇猜想"，范围收窄到真正站得住的部分。
为什么前沿模型会犯"低级错误"
知乎上这个问题的讨论很热，我的理解是这样的：这不是bug，这是天性。
大语言模型的本质是概率生成——它写的每一个符号，都是"在当前上下文里最可能出现的下一个token"，而不是"经过逻辑校验的正确答案"。绝大多数时候，"最可能"和"正确"重合，于是模型看起来无所不能。但在符号约定这种地方，+1和-1在语言概率上几乎等价，模型完全可能顺着语感选错一个，然后用同样流畅、同样自信的笔调把错误推演下去。
文章写得越漂亮，错误藏得越深。这正是AI产出和人类产出的关键差别：人犯符号错误往往伴随犹豫和涂改，AI犯错时笔迹一样工整。
OpenAI自己的解药也在这份更新日志里。研究员Dan Roberts在X上宣布，本轮新增6项Lean形式化，目前约42%的主要成果已完成形式化，剩下近58%还停留在人类可读的手稿阶段。Lean是机器证明助手，证明写成Lean代码、通过编译，才算机器可验证——相当于给数学证明装了一个"编译器"。符号写错，编译器直接报错，不给流畅的错觉任何生存空间。
换句话说，OpenAI用行动承认了一件事：模型的自我检查靠不住，必须交给外部的形式化验证。
普通人的"Lean"是什么
我们不证霍奇猜想，但每天让AI写方案、写代码、做表格时，面对的是同一个风险：它错得越流畅，你越难发现。
数学界的答案是形式化验证，普通人的答案朴素得多——给AI产出配一个"外部校验环节"。数据类的产出，回原始来源对一遍数字；代码类的产出，跑一次测试再说；文档类的产出，用版本记录留痕，每次大改写一句变更说明。核心原则只有一条：不拿"AI写得很顺"当"AI写得对"的证据。
我自己干活就是这个路数：在AI家园 spark1.cn/tools/ 里把多个工具串成固定流程，每一步的输入输出都摆在台面上，哪一环出问题能立刻定位——这就是普通人版本的形式化验证。
连OpenAI都要靠撤稿和编译器来兜底，我们用AI时多留一道校验，不是不信任AI，而是和它合作最从容的方式。产出可以交给AI，验证的最后一环，留在自己手里。
评论