2026年5月,一个由OpenAI训练的系统悄悄干了数学界惦记了80年的一件事——它生成的构造,推翻了Erdős关于平面单位距离问题的猜想。Nature很快以"AI攻克80年数学难题,研究者震惊"为题报道。几周之内,Noga Alon、Timothy Gowers等一批数学家发表后续论文,确认了这个反例站得住脚。故事听起来是一条纯粹的喜讯。
但数学家Jun-Yong Park在同期挂出的论文里问了另一个问题:如果这类突破继续加速,而美国正在削弱培养"能看懂AI在做什么的人"的体系,五年后还有谁能审核AI给出的数学结论?
反例有多硬,人类几周内就验完了
这不是一个模糊的"AI又解了道题"。新构造给出的下界是 n^1.014,足以打破此前"至多 n^{1+o(1)} 对单位距离点"的猜想图景——一个存续了80年的上界判断,被一个具体、可检验的数字击穿。
更值得记下的是验证速度。Alon、Bloom、Gowers、Litt、Sawin、Shankar、Tsimerman、Wang、Wood 这批数学家,在几周内就完成了对这个AI反例的人工复核并成书面论文;Will Sawin 还独立给出了一版自己的证明。这说明当前顶尖数学家的审核能力,至少这一次,没有掉队。
钱在收紧,而数学是AI理论的地基
同一时间段,美国联邦对数学科学的资助环境却在变紧。NSF 2026财年的预算申请总额降到39亿美元,NSF自己在材料里都用了"受限财政环境"这个说法。讽刺的是,NSF在同一份材料里,明确把数学列为AI基础理论投入所依赖的学科之一。
这里需要一句审慎的补充:39亿美元是预算申请,不是国会最终批准的拨款额度。两者之间历来存在落差,把申请数字直接等同于"已经砍掉的钱",是不严谨的。但申请本身释放的信号已经足够清楚——数学科学不是资助优先级正在上升的领域。
数学能力是基础设施,不是学科经费项目
Park论文里最关键的一个概念区分是:数学能力不等于数学产出。会证明定理是产出;能验证、解读、质疑一个证明是否成立,是另一种能力——受训多年才能长出来的能力,也是他称之为"基础设施"的东西。
他把这种能力和半导体产能放在一起类比:芯片制造能力一旦流失,不能靠一笔预算按需重建,需要的是设备、工艺积累和一代代工程师;数学审核能力同理,不是招几个博士生就能补上的缺口,而是院系、导师体系、资助项目长期堆出来的产物。
基于这个判断,Park提出一条具体的政策建议:执行关键推理的AI系统,应当被要求把决策性论断以形式化、机器可检查的方式暴露出来——把AI推理的一部分,从"说服你相信"变成"可以被程序核验"。这个思路目前只停留在单篇论文的倡议层面,还没看到对应的立法、行业标准或试点项目。对靠"黑箱"维持竞争优势的商业AI公司来说,这条建议天然缺乏推动它落地的动力。
我更在意的落差在哪
Park这篇论文最有力的部分,恰恰不是它最想强调的部分。他想说的是"管线正在被削弱",可这次反例验证给出的证据,反而是"人类还没掉队"——Alon、Gowers这批数学家用几周时间完成了复核,这个速度本身就是一种反例式的安慰。
真正该盯住的变量不是这一次,而是下一次。这次是一个高调、可被顶尖数学家集中围观的案例,才换来了几周内的快速验证。如果AI生成的研究级数学结论开始批量出现,而愿意投入时间去人工复核的顶尖数学家数量没有同步增长,验证速度和产出速度之间的剪刀差就会打开。届时资助被压缩的院系、萎缩的研究生名额,才会真正兑现成"看不懂"的后果。
《中庸》有句话叫"凡事预则立,不预则废"。Park这篇论文的价值,不在于证明危机已经发生,而在于提醒一件容易被忽略的事:审核能力是慢变量,补救永远来不及等到危机兑现那天再启动。这一次人类跟上了,不代表下一次还跟得上。