夜雨聆风三个月，AI 在数学上连下三城——可真正的考题不在算得对不对
2026 年的夏天，数学圈被 AI 搅得有点睡不着觉。
不是一次，是三次。五月底，OpenAI 把一个困扰学界几十年的猜想推翻了；七月中世界杯决赛夜，另一家公司的模型顺手又干掉了一个 87 年的老猜想；八月初，OpenAI 再甩出十项成果，号称两千美元、Lean 机器验证。
热闹是真热闹。但把这三件事摆在一起看，一条线越来越清楚——外界对 AI 数学的挑剔，已经从"你对不对"，悄悄挪到了"你干不干净"。
说白了，算得对，已经不够了。
第一城：五月，OpenAI 的封神时刻
五月底，OpenAI 的一个内部推理模型，把 Erdős 在几十年前提出的"单位距离猜想"给推翻了。
这事在数学圈分量很重。菲尔兹奖得主蒂莫西·高尔斯（Tim Gowers）直接说，此前没有任何 AI 生成的证明能接近这个水准。更关键的是，这个结果不是模型自说自话——九位顶尖数学家人工逐行审阅过，没人挑出毛病。
⚡ 五月这一仗，AI 数学是真正封了神的：结果对、人审过、零争议。
它怎么做到的？把一个代数数论里的工具，跨界用到了平面几何上。这种"人类压根没往这个方向想"的连接，恰恰是 AI 最吓人的地方——它不依赖既有文献，所以也没人能说它"抄了谁的"。
第二城：世界杯决赛夜，Anthropic 的 Fable 5 干了一件更猛的
六月到七月，美加墨世界杯踢得正酣。决赛那晚，全世界都在看球，一位在 Anthropic 工作的哈佛数学家 Levent Alpöge，顺手给自家模型 Fable 5 抛了个问题：
那个困扰数学界 87 年的雅可比猜想，到底对不对？
模型在后台跑了一阵，丢回来一个三元多项式。Alpöge 把它贴上了 X。
❝
这大概是迄今人工智能在数学证明或证伪方面，扮演重要角色的最大猜想。
— Abhishek Saha，伦敦玛丽女王大学
这个反例有多漂亮？它满足雅可比猜想的全部前提——雅可比行列式恒等于 −2，一个非零常数——可实际上它把三个不同的输入，全送到了同一个输出点。猜想说"局部处处可逆就必全局可逆"，Fable 5 直接用三条路撞死在同一扇门上，把它证伪了。
人类此前估计，这种反例怎么也得 200 次多项式才可能出现。Fable 5 给了一个 7 次的、能写进一条推文的构造。
更绝的是验证速度。Wolfram Alpha、SymPy、Lean 形式化证明，当天就把它验了个遍。雅可比行列式是不是恒为 −2？三个点是不是真撞到同一点？算一遍就知道，谁都能复现。
可这一步，恰恰暴露了 AI 数学的下一个软肋。
陶哲轩（Terence Tao）在结果出来第二天，专门发了一篇长文，反向重建了"为什么这个反例必然成立"的几何解释。因为 Fable 5 给的是"一个对象"，不是"一个理由"。
芝加哥大学的 Akhil Mathew 一句话点破：
❝
你能验证它的正确性，但它讲不出"为什么成立"的故事。
— Akhil Mathew，芝加哥大学
哥伦比亚的 Andrew Blumberg 更狠，打了个比方：这就好比摩西下山说"癌症能治"，可没带方法下来——你会在意吗？
⚡ 第二城的数学最干净——零署名争议。但它第一次把"AI 不知其所以然"摆上了台面。
当机器能造出对的东西，却说不清为什么——人类正卡在"替它补全理由"这道工序上。
第三城：八月初，Astra 十项成果，能力跃升却栽在纪律上
八月初，OpenAI 公布了一组由名为 Astra 的模型取得的十项数学成果，每个都配了 Lean 4 形式化证明。这里得把话说准：这不是一次正式的产品发布。OpenAI 给的是一个"下一代模型"的命名、一份 249 页的研究手稿和一组机器可校验的证明，却没给发布日期、没开 API、没放模型卡，模型至今仍关在内部安全评估和对齐阶段，外界连独立测一下都做不到。
按说这是三件事里验证最硬的一仗——机器证书比人类审阅还难挑刺。
可翻车（如果非要用这个词的话）不在数学，在别处。
叶史瓦大学的 Steven Miller 站出来说，Astra 在球堆积问题上的成果，核心论证其实来自他 2016 年的论文，OpenAI 没给够署名和引用。剑桥的 Fournier-Facio 也指出，Astra 关于非 sofic 群的结果，依赖的是 Kun 在 2016 和 2019 年的工作。
与此同时，OpenAI 官方公告里那句"这个问题至少十年没有进展"的表述，在八月初被悄悄撤下。
2026 年 AI 数学三连击
数学结果本身，至今没人推翻。Fournier-Facio 自己也承认，Astra 的核心命题是有创新的。争议严格卡在三个词上：引用、署名、话术。
一条越来越清楚的线
把三件事按时间排开，你会发现一个挺有意思的规律：
⚡ 当 AI 数学从偶发高光变成批量产出，外界的容忍阈值，已经从"正确性"抬到了"过程透明"，再抬到了"署名伦理"。
能力在涨，验证在硬，可审视的目光也在同步前移。Fable 5 正好卡在中间那一档：数学上最干净，却第一次让人看清，机器能造出对的东西，却说不清为什么——而人类，正卡在"替它补全理由"这道工序上。
那 AI 到底会不会做数学？
这个问题，现在还没标准答案。
五月的反证、七月的反例，都还停留在"推翻一个猜想"——找一个反例，否定一个全称命题，在结构上比"正面证明一个猜想"轻一档。真正难的，是建构新理论、讲出新故事。
但有一点已经变了：2026 年夏天之前，数学界讨论的是"AI 能不能辅助验证"。这三个月之后，讨论的是"AI 构造的可验证对象，已经大到人类自己都未必追得上"。
球赛会散场，猜想不会。下一次，被机器顺手解开的，会是谁家养了几十年的难题？