2026 年 10 月，在加州理工学院的讲台上，数学家陶哲轩抛出了一个反常识判断。现代 AI 正在把数学研究推入前所未有的怪圈。长达近一个世纪的「证明稀缺」局面，正在演变为「证明过剩」。
过去一个世纪，数学的根基压在一个前提上：证明很难得到。AI 正在把这个前提掀掉。解题原本是衡量学术进展的标尺，而现在，把刷题当成终极目标反而会掏空这门学科。
算力一年刷出 2200 万条命题，解题不再稀缺
传统数学建立在「证明稀缺」的前提之上。在过去一个世纪里，攻克一个公开猜想往往需要顶尖专家耗费数年心血。整个学术界的教职评审、期刊出版与声誉机制，都围绕这种稀缺性运转。
这种供需平衡正在被算力改写。陶哲轩在现场展示了真实的数据锚点。Equational Theories Project 在 2024 至 2025 年间，通过人机协作判定了通用代数中超过 2200 万条命题的真假。
图：Equational Theories Project 用众包方式判定了 2200 万条以上命题。来源：陶哲轩《Math 2.0》演讲幻灯片
类似的高频推进正在多个分支上演。在 2026 年的逆伽罗瓦问题挑战赛中，协作团队在短时间内为 24 次域的全部 25,000 个伽罗瓦群各算出一个多项式。随后，项目又将目标推向 31 次。
这种吞吐量颠覆了纯手工推导的传统工期。海量算力注入之后，数学研究正从针对孤立定理的个案解剖，转变为数据驱动的人口普查。
客观可验且无需实验，数学沦为大模型专属练兵场
为什么前沿 AI 实验室偏爱数学，远胜过生物学或社会科学？根本原因在于纯数学具备两项罕见的工程特质。
第一项特质是客观可验证性。数学家可以争论哪个猜想更重要，但对结论是否正确拥有坚实共识。借助 Lean 等交互式证明工具，计算机能在代码层面对推导进行机械核验。
第二项特质是高度可数字化。数学证明不需要物理载体，不需要真实世界的数据输入，也不需要实验来验证输出。纸笔、形式化数学库加上已经数字化的海量文献，机器学习就能在这个封闭回路里反复训练。
同时具备这三条的领域不多，前沿 AI 实验室因此把数学解题能力排在许多应用之前——毕竟刷题成绩既能被机器判定，又能在发布稿上写出漂亮的数字。
但模型的推理能力呈现出剧烈的锯齿状分布。投入充足算力后，模型能在无需专家协助的情况下攻克公开赛题；面对需要复杂交互与真实经验的现实任务，AI 依然容易卡壳。
社交媒体上的印象是另一回事：你看到的都是被 AI 解掉的题。陶哲轩提醒，当前数学前沿的大多数问题仍然没有被解决，即便烧掉大量算力也一样——数学问题的空间是无限的，难度没有上界。First Proof 这类平台就是为此建起来的，它要求把资源消耗和失败结果一并公开。
把终点当成全部，机器过早抵达会踩塌周边生态
在纯数学的世界里，公开问题并不只是一把等待撬开的门锁。陶哲轩给出了一个比喻：公开难题是一座座矗立在未知海域的灯塔。
灯塔的价值是照亮周边的航道。驶向它的过程往往比最终那个解答更有价值：成功、失败、只推进一半，留下的教训都算数。
图：Math 1.0 与 Math 2.0 的研究前沿演进。来源：陶哲轩《Math 2.0》演讲幻灯片
用自动化工具提前抵达灯塔，代价是没人走完中间的路。那些原本会在摸索中长出来的理论、工具和直觉，失去了出现的理由。解题与理解就此分家。
拿到了通过临床的癌症秘方，没人敢把液体打进血管
解题自古以来只是检验理解深度的代用指标。在证明稀缺的岁月里，攻克大题通常伴随着一套宏大理论的诞生；在证明过剩的时代，暴力求解让代用指标与核心目标直接脱钩。
陶哲轩在演讲中提出了一个思想实验。假设顶尖实验室训练出一个 AI 模型。它的目标很明确：交出一套能通过三期临床试验的抗癌药方，中途不许出错。
在消耗大量算力后，模型交付了一种未知的化学配方，并附带了严密代码证明。在真实测试中，该配方确实通过了试验。然而，没有任何科学家知晓它的分子机理。
当你自己被诊断出早期癌症，机器把这个配方推荐给你，在把药液推进血管之前，你是否希望至少有一个人——哪怕只是部分——理解它为什么有效？
纯数学的验证机制，终究要向现实世界转移。如果研究者习惯了在黑盒答案面前放弃思考，应用科学的安全底座也将被悄然瓦解。
陶哲轩开出药方：把算力从刷题挪向帮人理解
面对机器带来的过剩危机，陶哲轩给出的方案是转向 Math 2.0。核心诉求是将工具的重心，从单向刷题转移到强化人类理解上。
所谓「开放阐述问题」是一类新目标：为那些证明已知、但过程晦涩的结果，寻找有动机的解释。加州理工改版后的 Mathathon 就是这个方向上的一次实验。
研究网络与代码库的建设同样在加速。显式解析数论网络将零散的学术论文编织成知识图谱；形式化数学库 Mathlib 则为算法检验提供了标准底座。
研究人员开始利用算力进行定理消融实验。通过拿掉某个定理的关键前提，观察结论能否维持；或者放宽输入条件，探索定理周边的衍生空间。
这些尝试把算力用于提炼新方法，让人类看清知识地图的脉络。
在陶哲轩看来，推进 Math 2.0 的主要瓶颈是想象力——它排在算力和机构文化的前面。
参考链接：
- 陶哲轩加州理工演讲《Math 2.0》讲义与幻灯片
- First Proof 形式化数学评测平台 (1stproof.org)
- Equational Theories Project 众包研究项目归档
- 逆伽罗瓦问题挑战赛 (IGP24) 协作记录
