人工智能正在进入数学最核心的领地。过去，人们习惯把计算机视为高速计算器或证明检查器，如今，新一代模型已经能够提出证明思路、搜索反例、形式化复杂论证，甚至直接参与开放问题研究，这让数学界第一次认真面对一个令人不安的问题：如果机器也能“做数学”，人类数学家的价值将转移到哪里？
《新科学家》把这种变化称为数学史上最好也最糟糕的事情，并不夸张。AI正在拆除研究中的一些古老瓶颈，但也可能把数学推入一个答案过剩、理解不足的新阶段。
从解题工具到研究伙伴
过去几年，AI数学能力的进步并非只是考试分数上涨。DeepMind等团队已经把大模型与搜索、程序执行和形式验证结合起来，使系统能够在可自动检验的空间中反复提出候选解，再淘汰错误路线。
AlphaEvolve就是这种变化的代表。它让语言模型生成算法，再由自动评价器运行和评分，通过类似进化搜索的方式不断改进候选程序；这种机制已经用于矩阵乘法、组合数学和计算基础设施优化。
更重要的变化来自形式数学。
Lean等证明助手要求每一步都被机器严格检查，因此大模型常见的“看起来合理但其实错误”不能轻易蒙混过关。2026年的研究显示，AI驱动的形式证明搜索已经能够自主解决一部分公开的埃尔德什问题和OEIS猜想，这意味着AI开始跨过“会答题”与“参与研究”之间的门槛。
数学家过去最稀缺的是找到证明的时间。现在，机器能够同时搜索成百上千条路线，很多过去因为人力有限而不会被尝试的方法，正在变得廉价。
“证明丰裕”也可能制造知识拥堵
陶哲轩把正在到来的局面描述为从“证明稀缺”进入“证明丰裕”。这听上去像数学家的黄金时代，却隐藏着一个反直觉的问题：证明越容易产生，人类越可能来不及理解它们。
数学研究并不是把“已证明”三个字贴在一个命题上就结束。
一个重要结果还需要检查其意义，找到更简洁的核心思想，与已有理论建立联系，经过同行评议，再被写进教材和下一代研究者的知识体系。如果AI每天产生海量正确但冗长、难读、彼此孤立的结果，瓶颈就会从“能否证明”转变为“哪些值得理解”。
这种风险在形式证明中尤其明显。机器可以检查数百万甚至上千万行形式化代码，确认逻辑上没有漏洞，但一个在人类看来几页就能表达的数学思想，如果被展开成巨大的机器证明对象，正确并不自动等于可理解。
于是数学可能出现一种前所未有的“知识消化不良”：定理越来越多，真正进入共同理论结构的思想反而跟不上。
这种变化甚至会反过来影响学术评价。过去，发现一个新结果天然具有稀缺性；未来，如果机器能批量生成正确证明，真正困难的任务可能变成筛选、解释和建立统一框架。
最危险的不是错误，而是失去理解
人们最熟悉的大模型风险是幻觉，但对数学而言，错误反而是相对容易处理的一类问题，因为形式验证可以充当最终裁判。
更深的难题是数学的目标究竟是什么。
如果目标只是得到真命题，那么超级强大的证明机器显然是进步；但数学同时追求解释、结构、简洁性和可迁移的思想。一条证明之所以重要，往往不是因为它告诉我们某个命题为真，而是因为它揭示了为什么为真，并由此打开新的领域。
近期AI数学突破已经让这种张力变得现实。AI系统可以快速探索复杂证明空间，而人类可能逐渐退到提出问题、验证结果和解释意义的位置。
这并不必然意味着数学家会被淘汰，却意味着职业定义正在改变。未来更稀缺的能力可能不是手工完成漫长推导，而是选择值得研究的问题，判断机器结果是否重要，把孤立结论压缩成概念，并发现不同领域之间真正有价值的连接。
数学正在成为AI时代的试验场
数学之所以比许多科学领域更早感受到冲击，是因为它拥有AI最喜欢的环境：规则清晰、答案可验证，而且很多任务可以被形式化。
在实验生物学或材料科学中，一个模型提出新假说后仍需要昂贵实验；在形式数学里，正确性能够由证明检查器在计算机内部完成。这使数学成为训练“研究型AI”的天然试验场，也让进步速度尤其快。
但这种优势也可能把学术制度推到极限。论文数量、作者资格、AI贡献披露、研究优先权以及训练数据来自哪里，都正在从技术问题变成学术伦理问题。
更棘手的是教育。如果学生过早把推理交给模型，他们可能获得答案，却失去形成数学直觉所必需的挫折、试错和长期思考。
因此，AI对数学最深刻的影响或许不是“机器会不会取代数学家”，而是迫使数学界重新回答一个古老问题：数学究竟是在生产答案，还是在生产理解？
如果未来证明真的变得像计算资源一样丰富，真正昂贵的东西将不再是一条新证明，而是能够让人理解它、判断它为什么重要并把它变成下一代思想起点的人类判断力。AI可能成为数学史上最强的放大器，而它最终放大的究竟是知识还是噪声，将取决于数学共同体如何重新设计研究、评价与教育规则。
上述关键事实已结合原报道简介、2026年AI形式证明研究、陶哲轩关于“证明丰裕”的讨论以及DeepMind公开技术资料交叉核对。
