陶哲轩预言“数学2.0”：AI辅助证明重塑数学研究范式

在数学界，菲尔兹奖得主、加州大学洛杉矶分校教授陶哲轩（Terence Tao）一直是“AI辅助数学”最坚定的推动者之一。他近期再次公开阐述了自己的判断：一个由AI与形式化验证共同驱动的“数学2.0”时代正在到来，数学研究的工作方式将迎来自现代公理化体系建立以来最深刻的变革。

从“数学1.0”到“数学2.0”

陶哲轩把人类沿用数百年的数学工作方式称为“数学1.0”：数学家在纸上或黑板上手工推导，同行评审是主要的质检环节，一篇重要论文从完成到正式发表往往需要数月甚至数年。这个体系产出了辉煌成果，但效率瓶颈也十分明显——证明的可靠性依赖审稿人的仔细程度，而错误有时多年后才被发现。

在他描绘的“数学2.0”图景中，数学证明将逐步与形式化验证系统（如Lean等证明助手）结合，AI大模型承担起草证明、填补细节、检索已有结论等繁重工作，而人类数学家则专注于提出问题、把握方向与判断证明的美感与意义。人机分工的界面，将从“纸和笔”变为“对话和代码”。

AI是“副驾驶”而非替代者

陶哲轩多次强调，至少在可预见的未来，AI不会取代数学家，而是扮演类似飞行员副驾驶的角色。他把大模型比作一个“知识渊博但不够可靠的合作者”：它读过几乎所有公开的数学文献，能快速给出思路提示，但也会一本正经地犯错，因此每一步都必须经过形式化验证的把关。

AI不会替你做数学，但会极大地降低你做数学的门槛——就像计算器没有取代数学家，却改变了每个人与数字打交道的方式。

这一判断与他此前的公开表态一脉相承。他曾预测，到2026年前后，AI若与形式化证明工具结合，将成为数学研究中可信赖的工具，甚至可能在部分领域比肩顶尖研究生的辅助能力。如今他持续观察到的大模型在数学推理上的快速进步，正在印证这一预测的方向。

实验与试点：证明正在发生的变化

陶哲轩本人就是最早“吃螃蟹”的人。他曾在著名的多项式平均定理（Polymath式协作项目中的不等式证明）研究中，借助AI辅助与Lean形式化验证，将原本预期耗时数周的证明流程大幅压缩，公开演示了“人提出思路、AI补全细节、机器验证正确性”的完整闭环。这一案例被广泛视为AI辅助数学的里程碑。

与此同时，社区层面的大规模协作也在提速。由数学家们发起的“公理”（Aristotle／formalization）式在线协作项目，吸引了全球数百名贡献者参与，其中相当一部分工作由爱好者和学生完成——他们借助AI工具和证明助手，首次能够真正参与到前沿数学的形式化进程中。陶哲轩认为，这种“众包+AI”的模式，可能是未来数学产出的重要形态。

学界的期待与争议

并非所有人都对“数学2.0”持乐观态度。一些数学家担心，过度依赖形式化和AI会让数学丧失直觉驱动的美感，年轻研究者可能学会“生成证明”却不再理解证明背后的思想。也有人质疑，目前大模型在真正前沿的数学难题上仍力不从心，AI辅助更多停留在整理与验证层面。

支持者则反驳说，形式化历史上也曾遭遇抵触，如今已成为数学基础研究的标准工具之一。计算机辅助证明的经典案例，如四色定理和开普勒猜想的证明，当年都曾引发“这算不算真正的证明”之争，而最终数学界接受了机器验证的价值。陶哲轩认为，AI引发的争议将是同一段历史的重演，且这一次融合的速度会更快。

影响分析：从科研到教育的连锁反应

如果“数学2.0”成为现实，其影响将远超数学界内部。首先是科研效率：证明的验证周期从“以月计”缩短到“以小时计”，审稿人可以把精力从核对细节转向评估价值，数学成果的产出速度有望显著提升。

其次是数学教育与研究门槛的改变。AI辅导系统可以让更多学生和跨学科研究者接触到严格证明，形式化证明库将成为可检索、可复用的“数学基础设施”。陶哲轩设想，未来数学知识可能以机器可验证的形式沉淀下来，形成全人类共享的、永不失真的数学知识库——这也是他眼中“数学2.0”最深远的遗产。

展望未来，陶哲轩呼吁数学界主动拥抱工具变革，同时保持清醒：AI提供的是速度与可靠性，而问题的重要性、方向的判断与数学的美，仍将由人来决定。人机协作的数学新范式已经起步，它最终能把数学带向多远，取决于 mathematicians 与工程师接下来几年的共同努力。