陶哲轩提出"数学2.0"：当AI让证明变得泛滥

当"证明稀缺"的时代走向终结

菲尔兹奖得主陶哲轩抛出了一个足以撼动数学界的判断：建立在"证明稀缺"之上的数学1.0时代即将落幕，数学2.0时代已经到来。这一论断的背后，是AI对数学研究节奏的剧烈冲击。

在传统的数学1.0时代，证明一直是稀缺品。要攻克一道开放难题，研究者往往需要深厚的专业积累，并为此投入大量时间与精力。正因如此，"谁最先解决了什么问题"自然成了衡量数学贡献的核心标准。但当AI能够在短时间内批量输出证明时，这套评价体系的根基开始松动。

据量子位报道，陶哲轩在加州理工的最新演讲中正式阐述了这一观点。有意思的是，这篇演讲稿原本的主题是《机器辅助证明》，但在近期AI频频"轰炸"数学界的背景下，他不得不把主题调整为《数学2.0》——这种临时转向本身，恰恰生动地印证了AI加速带来的冲击。

陶哲轩：数学2.0时代已至

数学为何如此容易被AI攻破

陶哲轩归纳出三个相互叠加的条件，解释了数学为什么会成为AI能力突飞猛进的核心战场：

证明可以被客观检验：对错有明确标准，不依赖主观判断；
数学对象和推理过程高度可数字化：天然适合机器处理；
大量高质量研究文献已以数字形式存在：为模型训练提供了充足养料。

这三者叠加，再加上前沿AI实验室的巨额投入，便把数学迅速推成了模型练兵的理想战场。无论是OpenAI一夜甩出722篇数学论文、扫射准黎曼猜想、霍奇猜想、BSD猜想等重磅研究，还是把王虹刚获菲尔兹奖的三维挂谷集维数猜想进一步扩展到四维，都在改写数学研究的节奏。

不过，陶哲轩并没有被这些成功案例冲昏头脑。他亮出那张经典的"飞机弹孔图"，提醒人们警惕"幸存者偏差"：数学前沿的大多数问题依然悬而未决，AI的能力并不均匀，在某些方向惊艳，在另一些方向仍然乏力。AI厂商展示的往往是精挑细选的成功案例，而海量失败的尝试压根没机会进入公众视野。

透明评估：失败和算力成本都该被报告

只统计成功的做法，无法回答成功率、资源消耗和人类参与程度这些关键问题。基于此，陶哲轩呼吁建立一套更透明、更科学的评估机制，把失败结果和AI算力成本一并纳入报告。

这一诉求直指当下AI数学宣传的痛点。当一个实验室宣称"解决了某难题"时，外界往往无从知晓它尝试了多少次、烧掉了多少算力、人类研究者又在其中扮演了什么角色。缺乏这些信息，所谓的"突破"就难以被科学地评估和复现。

但陶哲轩显然认为，仅仅拿出正确证明、报告失败与成本还远远不够。真正的问题在于：越来越多的AI证明，能否为人类带来更多理解、更好的训练，以及对现实世界更可靠的贡献？

盲目卷"解题"会损害数学的长期健康

陶哲轩用了一个形象的比喻：开放问题就像灯塔，它们指引人们探索周边的数学世界，而抵达灯塔并不等于完成了探索。

在他看来，尝试解决问题的过程——无论成功、失败还是部分进展——都可能产生比最终答案更有价值的认识。如果自动化工具过早交出答案，而评价体系又只奖励"已解决"，那些尚未走过的路径就会失去被探索的动力。他特别强调：千禧年大奖难题是有限的，但由一个问题生长出的路径、理解、联系和新问题，却几乎是无限的。

正因如此，他警告道：如果继续盲目优化"解题"这一单一指标，将会损害数学的长期健康。这也解释了他在SAIR演讲中为何如此不留情面地向模型公司开火——"AI公司无休止地加速，却对那之后会发生什么一无所知，我们必须慢下来"。

事实上，这份担忧早在今年9月初就出现在他的博客评论中：AI可以成为服务数学研究的工具，但追逐短期目标可能以牺牲数学共同体的长期可持续性为代价。

千禧年大奖难题（Millennium Prize Problems）是克雷数学研究所于2000年设立的七道悬而未决的数学问题，每道悬赏100万美元，包括黎曼猜想、P vs NP、霍奇猜想、BSD猜想（贝赫和斯维讷通-戴尔猜想）等。迄今为止仅有庞加莱猜想被格里戈里·佩雷尔曼解决（他拒绝了奖金）。这些问题之所以被称为"灯塔"，不仅因为其极端困难，更因为围绕它们发展出的理论工具和数学结构往往远比最终答案本身更有价值——例如怀尔斯证明费马大定理的过程催生了大量模形式与椭圆曲线理论的深刻发展。陶哲轩担忧的正是：若AI优先"摘果"而非"开路"，这些附带生长出的知识生态将因缺乏探索动力而枯萎。

"癌症疗法实验"：人类理解为何不可替代

为了说明人的理解为什么仍然重要，陶哲轩提出了一个颇具冲击力的思想实验。

假设你让先进AI去寻找一种能通过三期临床的癌症疗法。烧完算力后，它给出了一组未知化学物质的混合物：模型预测能杀死癌细胞，Lean形式化验证通过，三期临床也过了。但没人知道它是怎么找到的，也无法确定AI究竟是真找到了疗法，还是钻了试验流程的空子。

在针扎进血管之前，你是否会希望——至少有一名癌症专家能理解它的作用机制，一名数学家能看懂背后的数学推理，一名科学家能读懂那个寻找疗法的模型？

这个实验把抽象的数学讨论拉进了具体场景：模型内部的结论即便通过了验证，仍然需要有人判断它与现实世界的目标是否一致。模型可以生成答案、验证推理、加速探索，但不能替人类把关——这或许正是人类科学家不可被取代的关键。

证明的五个阶段与"证明消化不良"

在此前发布的《AI时代的数学》中，陶哲轩把解题拆成了五个阶段：

生成证明；
验证正确性；
解释清楚；
被共同体理解和接受；
最终融入领域的标准理论。

其中最后一步尤其缓慢：研究者需要找到更自然的表述、更合适的证明，把结果与其他知识连接起来，才能让它进入教材、成为下一代数学家的工具。而这恰恰是AI很难加速的环节。

如果AI主要加速前面几步，后面就可能出现"证明消化不良"。因此陶哲轩主张：减少对"抢先生成证明"的强调，增加对解释、评审和知识整理的重视。他甚至认为，仅有形式化验证远远不够，作者还应该能把成果讲清楚，否则这样的成果仍是不完整的。

这一立场在10月初的争论中达到高潮。10月7日，OpenAI一口气发布722篇数学论文，彻底激怒了以陶哲轩为首的"AI减速派"。他随即牵头成立"人类数学协会（AHM）"，发布联合声明，批评一次性发布700多个文件"根本不算科研，纯粹是在炫耀算力霸权"，并敦促数学家停止与OpenAI合作，回归以人类理解为核心的科学愿景。

Lean是一种交互式定理证明器（Interactive Theorem Prover），用于将数学证明形式化为计算机可验证的代码。数学家用Lean书写的证明可以被机器逐步检查，确保每一推理步骤都符合公理系统，从而消除人工审查中的疏漏。近年来，形式化验证被视为AI辅助数学研究的重要基础设施——AI生成候选证明，Lean负责核验。然而陶哲轩指出，形式化验证只解决了"正确性"问题，并不等于"可理解性"。一个通过Lean验证的证明可能逻辑无懈可击，却让任何人类读者都无从获得直觉或洞见。这正是他批评"仅有形式化验证远远不够"的核心所在：证明需要能被数学共同体吸收、复用和教授，才算真正完成了它的使命。

AI时代，数学还需要读博吗

这场争论也戳中了年轻研究者最关心的问题：如果AI能快速生成论文，读研读博还有没有必要？

陶哲轩的回答颇为清醒：读博的价值不在于能不能产出论文，而在于能否培养出一套"吸收困难材料、综合知识、提出好问题"的系统能力。

他用饮食和运动作比方：当食物和交通充裕后，人得自己学会运动；当答案随手可得后，人也要有意识地维护认知能力，禁得住绕过思考的便利——而这些恰恰是博士培养的核心能力。如果你只是为了产出成果，AI时代读博的必要性确实在下降；但如果你希望被训练成能啃硬问题、能综合知识、能提出好问题的人，读博依然有其价值。

另一边，陶哲轩也在身体力行地探索人机共进的路径。他参与创立的SAIR基金会推出了"开放数学模型计划"，第一阶段面向日常研究需求，如理解困难论证、核查引用、探索例子、编写代码以及形式化证明等，相关模型即将发布。

SAIR（Science and AI Research）基金会是陶哲轩参与创立的非营利机构，旨在探索AI与基础科学研究协作的可持续路径，与OpenAI等以商业利益驱动的AI实验室形成对照。"开放数学模型计划"的定位是面向日常研究工作流的辅助工具，而非以"解决千禧年大奖难题"为噱头的竞赛型模型。这一方向的选择本身即是陶哲轩理念的体现：AI最大的价值不在于抢先给出答案，而在于帮助数学家更高效地理解论证、探索例子、整理知识——即服务于证明五阶段中后半段那些被当前AI热潮所忽视的环节。

瓶颈不是算力，而是想象力

在演讲结尾，陶哲轩把实现数学2.0的主要瓶颈归结为——想象力。

证明的供给正在发生根本性改变，但如何利用这种变化，把理解、训练和探索一起向前推进，仍需要数学界共同作出选择。当一道题被AI证明之后，数学家的下一个问题或许将是：从这个答案中我们还能学到什么？接下来我们还能做什么？

从"谁先解出题"到"解出题之后我们理解了什么"，这或许正是数学2.0时代最深刻的范式转变。AI改变的不只是证明的生产方式，更是在逼迫整个学界重新定义：究竟什么才是一位数学家真正的护城河。