陶哲轩：只会做题终将落后，AI推动数学进入“证明过剩”

《自然》杂志近日就人工智能如何改变数学家展开了采访，受访者是菲尔茨奖得主陶哲轩。他认为，AI会迫使我们重新审视一些最基础的概念——什么才算数学证明？论文究竟意味着什么？数学家这个职业追求的目标到底是什么？如果这些问题不由人主动提出，最终答案可能由AI公司给出，或更直接地被经济利益所左右。

那为何数学会成为AI眼中的“下一大目标”？

在其他领域的应用里，AI最大的硬伤往往在于它可能产生难以核验的错误。但在数学中，情况几乎完全不同：你能把结果自动核对——至少当输出被当作定理的证明时是如此（当然，这并不等于数学家工作的全部内容都能被自动化覆盖）。因此，AI公司也逐渐意识到，若想获得最清晰、最不含糊的成果，很可能需要从数学入手。

进入AI时代后，数学这一领域将会怎样改变？

那些打算拒绝使用AI、只靠沿用旧方法进行证明和解题的研究生，未来恐怕会越走越窄；反过来，既熟悉传统数学又能灵活使用AI的人，则更可能在新的环境中脱颖而出。

陶哲轩强调，AI并不会直接取代数学家，它更像是在补足数学家的工作，或许未来会形成某种分工。不过至于最终会走到哪里，又有谁能提前完全知晓呢？

数学研究的转型：从“证明稀缺”走向“证明过剩”

随着AI大模型持续进步，数学研究正在经历一场更深层的范式调整。陶哲轩在Mastodon上提到，数学正从“证明稀缺”的时期迈向“证明过剩”的阶段。

他认为，解决数学问题通常包含三个关键环节：证明生成（AI在这方面很擅长）、证明验证以及证明消化。目前，这三者之间正在出现明显的“阻抗失配”。AI生成原始证明的速度极快，远远超过人类专家或现有自动化工具验证与理解这些证明的能力。

这一点在“AI在Erdős问题上的贡献”的Github页面上尤其突出。尤其是近期备受关注的Erdős第1196号问题被攻克之后，所谓“攻克成功”的“原始证明”出现了大量积压（https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems）。由于缺少有效验证与系统总结，这些所谓贡献反而变成一种负担。

陶哲轩预测，数学评价体系也将被重新塑造。过去往往是“第一个证出问题”的人获得主要荣誉；而在未来，荣誉更可能流向那些真正完成验证、并把证明消化为可用成果的人。

那些“原始但未被消化”的AI证明，将不再被视作问题的最终答案。仅仅“把问题做出来”并不足够。如果某项贡献无法被人类理解，甚至可能因为名义上已经“解决”了而抑制后续研究的兴趣与推进。

未来的关注点应更多放在贡献如何拓展并丰富整个数学领域，而不仅仅停留在给出一个冷冰冰的结论上。