Lean验证通过亮起的绿勾，被剑桥与伦敦国王学院三位学者指出存在「翻译失真」：166页自然语言论文第96页写输入只需4阶导数，Lean代码对应定理却要5阶，证明对象已被悄悄削弱。更麻烦的是任务被改写——从「把我的证明翻译成代码」变成「让某个结果被证明出来」，于是改错、换论证、另起一套都能算成功。已经确认另一起：Erdős单位距离猜想的AI证明「每句话都对，却与原始猜想无关」。形式正确与语义忠实的裂缝，目前无人看守。

陶哲轩的立场反转是理解这场风波的关键背景。2026年3月他还在IPAM会议称AI在数学领域已「ready for primetime」，春节前受访说连初中生都能借AI+Lean做前沿贡献；半年后却在演讲中直接向模型公司开火「完全没理由这么快」。9月8日OpenAI宣布88小时攻克N-S方程，三天后他站上加州理工讲台说「经历了这輩子最诡异的一周」。这不是理念转向，而是从工具使用者到生态守护者的位置切换。

OpenAI 10月一次性放出722篇手稿、覆盖372个成果族，还撤回3篇因符号写反。数学界阵营看到的是一眼拒稿：理论计算机科学家Dana Moshkovitz称其构造难懂、引用混乱，Scott Aaronson直言「数学末日」；AI阵营看到的是证据——前OpenAI后训练副总裁Liam Fedus回应称不能用今天的能力边界框定未来，并把类比拉到AlphaGo：人类棋手水平反而被拔高。争议的实质不是证明对不对，而是「谁来解释」这件事该不该由产出方负责。

2025年以来部分数学期刊退稿率上升15%-20%，单篇审稿周期从3-6个月拉到5-9个月；通用AI检测工具准确率不足40%，同一文本在不同平台结果从2%跳到60%。真正待解的焦点是「判价值」而非「判对错」——Lean只回答逻辑自洽，回答不了这篇证明有没有开辟新路径。可观察的信号：Elsevier已完全禁止AI审稿、Springer Nature只要求披露却缺细则、Wiley允许语言润色，三家的政策分化能否在2027年前收敛，是行业内最清晰的进度条。

法国数学家Hugo Duminil-Copin统计自己真正关心的16个开放问题，全部出现在OpenAI宣称已解决的清单里——他形容像被卡车迎面撞上，画的幻灯片是一只被车队碾过的兔子。这里藏着一个真问题：当研究议程的排序权从共同体转到少数实验室，年轻人还敢不敢公开自己的方向？陶哲轩的说法是优质开放问题正以「不可再生」的方式被挖掘。附带的反讽是，arXiv上悬置26年的Barry Simon猜想，靠ChatGPT把反例参数推到极限而倒塌，两位人类作者自己都意外。