AI时代的数学工作流重建

摘要

陶哲轩讨论了AI、形式化证明和协作平台正在改变数学研究方式。数学正在从证据稀缺走向证明过剩，问题不再只是能否证明，而是证明能否被理解、复用、教学、审查，并推动领域继续前进。未来数学需要新的工作流和基础设施。

内容框架与概述

陶哲轩先把数学与其他科学作对比。其他领域已经经历大科学、数据爆炸和大规模协作，而数学仍主要依赖少数人在黑板前工作、写论文、同行评审、教学传播。AI带来的变化不只是更快地解题，而是让数学进入证明泛滥的时代，传统审稿、教学和论文系统会承压。

核心问题在于，数学项目有显性目标，也有隐性目标。显性目标是证明一个定理、解决一个猜想；隐性目标包括解释关键思想、关联文献、提炼方法、训练研究者、让后人能继续使用。AI可能完成显性目标，却没有完成这些隐性目标，于是会出现技术上正确、但没人真正理解和使用的证明。

后半部分转向新工作流。陶哲轩讨论了Polymath式众包项目、Lean形式化项目、GitHub与持续集成、AI代理辅助证明等方案。他主张区分不同数学场景：有些任务只需要验证真假，可以让AI高速处理；有些任务必须由人类协调，保留可读性、可复用性和教育价值。数学真正需要的是道路系统，不只是更快的车。

核心概念及解读

New mathematical workflows，新数学工作流

传统数学工作流以小团队、论文、审稿、课堂为中心。新工作流则要容纳AI生成、形式化验证、多人协作、任务分解、自动化检查和开放讨论。问题不再是把AI塞进旧流程，而是重新设计流程本身。

Proof flood，证明泛滥

过去数学长期处在证据稀缺状态，找到证明很难。AI和形式化工具提高了生成证明的能力，未来可能出现大量证明。瓶颈会从生成证明转向理解证明、筛选证明、消化证明和组织证明。

Explicit goals and implicit goals，显性目标与隐性目标

显性目标是把题做出来。隐性目标是解释为什么这样做、关键想法在哪里、和已有文献有什么关系、能不能教给学生、能不能迁移到别的问题。AI容易盯着显性目标跑，数学共同体则必须守住隐性目标。

Proof digestion，证明消化

一个证明刚出现时，往往复杂、粗糙、难讲。经过后续论文、讲义、课程和教材，它会被简化，核心思想会被提炼。AI时代的难题是，证明生成速度可能远超证明消化速度，导致数学交通堵塞。

Formalization，形式化证明

形式化证明通过Lean等系统检查证明的正确性。它能减少人工逐行审查的压力，但正确性只是底线。好的形式化项目还要考虑代码是否优雅、可读、可复用，能否融入已有库，而不只是拿到一个验证通过的标记。

Polymath projects，众包数学项目

Polymath项目通过博客、维基等工具让多人共同攻克问题，优势在广度和开放过程。它能展示真实的问题解决过程，包括失败路线、尝试过程和协作筛选。AI时代可以继承这种精神，但需要更现代的任务管理和自动化基础设施。

文章基本信息

字段	内容
原标题	Terence Tao: New mathematical workflows
作者	陶哲轩
发布日期	2026 年 5 月 13 日

陶哲轩关于新数学工作流的完整话题梳理

1. 数学正在从解题问题变成系统问题

1.1 AI辅助数学不能只看单个问题

当下很多AI数学进展集中在一个层面：解决某个猜想、完成某个证明、写出一篇论文。但数学不是孤立定理和论文的集合，它背后还有一整套系统，包括问题选择、证明理解、同行评审、教学、文献整理、后续研究和学术共同体的训练。

所以真正的变化不只是AI能不能证明一个定理，而是数学整体流程会怎样被AI改变。单点优化可能和系统优化发生冲突。一个工具把某个问题做出来，并不等于数学共同体真的吸收了这个结果。

1.2 数学工作方式长期变化很慢

数学过去几百年的基本工作方式没有发生根本改变。语言、会议设备、通信工具变了，但核心场景仍然是少数数学家一起讨论、写证明、投论文、等待审稿，再通过课程和书籍传播。相比之下，其他科学领域已经经历了大规模协作、数据爆炸和跨学科工程化。

这让数学在AI时代显得有些滞后。旧系统适合人类缓慢地产生数学成果，却不一定能处理机器快速生成的大量证明、候选结果和形式化代码。

2. 从证据稀缺到证明泛滥

2.1 过去的数学难在找证据

传统数学长期处在证据稀缺状态。一个问题有没有方向、有没有可行方法、有没有关键引理，往往都要靠少数人长期摸索。证明是一种稀缺品，所以整个学术系统围绕稀缺证明建立起来。

AI和形式化证明工具正在改变这一点。未来的问题可能不再是有没有证明，而是证明太多、太粗糙、太难理解、太难消化。

2.2 证明数量增加以后，瓶颈转移了

当证明生成能力变强，瓶颈就转移到几个地方：谁来判断这些证明重要不重要，谁来检查它们是否真的正确，谁来解释关键思想，谁来把复杂证明变成可以教学和复用的知识。

形式化验证可以帮助剔除错误证明，但正确性只是底线。数学还需要可读性、结构性、文献关联、思想提炼和进一步问题。只靠一个Lean验证通过的标记，不能替代完整的数学理解。

3. 显性目标和隐性目标的分离

3.1 显性目标是把题做出来

一个数学项目通常有一个表面目标：证明某个定理，解决某个猜想，回答某个问题。这类目标很容易被量化，也很适合AI优化。只要证明成立，形式化系统通过，显性目标就完成了。

3.2 隐性目标才是数学共同体真正依赖的东西

数学项目还会自然产生很多隐性目标。比如弄清楚这个猜想和过去文献的关系，识别真正困难的步骤，比较不同方法的优劣，提炼新技术，找到后续问题，训练作者和读者的能力。

人类做数学时，这些隐性目标往往顺手完成。因为人在证明过程中会记录困难、寻找引用、解释动机、总结失败路线。但AI可能只交出一个结果，不解释来源，不突出新思想，不训练任何人，也不帮助后续研究继续推进。

3.3 AI可能完成题目，却没有推进领域

最糟糕的情况是，一个问题被AI解决了，但没有人能讲清楚这个证明，没人能回答听众问题，没人知道怎么把它用于别的问题。问题表面上结束了，领域却没有真正前进。

陶哲轩给出的判断标准很直接：不要只问证明是否生成、是否验证，而要问有没有人能围绕它做一次讲解，并回答听众的问题。这个标准比一个验证标记更接近数学共同体真正需要的成果。

4. 同行评审和证明消化会遇到压力

4.1 传统同行评审处理不了AI规模

过去人类论文也会有问题。有些证明正确，但解释不好，思想不清楚，对下一代训练帮助有限。传统系统依靠审稿人、后续论文、讲义、教材和课程来慢慢修正。

但如果AI参与后产生大量证明，人工审稿人无法逐篇处理。最重要的结果也许还能被认真审查，大多数结果会进入无人能细看的状态。

4.2 证明消化变得更重要

一个证明刚出现时，常常复杂、粗糙、技术细节很多。经过后续整理，主要思想会被提取出来，最后变成研究生课程里能讲的内容。这个过程可以叫证明消化。

AI时代的问题是，证明生成速度可能远远超过证明消化速度。于是数学共同体会面对大量已证明但未理解的东西。它们占据文献空间，却没有变成真正可用的知识。

4.3 AI评分器只能作为辅助过滤

可以让AI评估论文是否有趣、引用是否完整、证明是否可信，但这不能作为主要防线。奖励作弊会成为严重问题。AI系统如果知道评分标准，就可能生成符合评分器偏好的内容，而不是生成真正有价值的数学。

5. 汽车和道路的比喻：AI能力不是基础设施

5.1 更快的车不能自动改善交通

AI技术像汽车，让个体移动速度突然提高。但数学的期刊、课程、教材、审稿制度、学生训练方式，还像汽车出现前的街道。只改进汽车，不修道路，交通可能更堵。

这比喻很准确。AI能让个人更快地产生证明，但如果没有新的协作协议、验证机制、文献整理方式、教学流程和成果评价标准，整个数学系统反而会更混乱。

5.2 数学需要区分不同道路

有些地方可以开放AI高速行驶，有些地方适合有限辅助，有些地方仍然要保留人类主导。比如纯粹为了确认某个命题真假，可以允许AI大量尝试；但涉及规范证明、教学材料、核心理论结构时，就不能只追求速度。

这不是反AI，而是要给AI分配合适的位置。车可以上高速，但不能开进教室。

6. Polymath项目：AI时代之前的众包数学实验

6.1 Polymath擅长广度，不擅长孤独突破

Polymath项目通过博客和维基组织多人在线协作，一般有十几到几十人参与。它最擅长利用广度：不同领域的人带来不同经验，帮助识别某个问题和优化、代数几何、组合数学等方向的联系。

这类项目未必能替代某个数学家长期孤独思考后得到的深层突破，但它很适合优化已有证明、改进边界、寻找联系、快速筛选大量路线。

6.2 它展示了真实的数学过程

普通论文和演讲经常展示一个 polished 的成功版本。失败尝试、死路、修正过程、误判和临时想法都被清理掉了。Polymath项目因为过程公开，让学生和年轻研究者能看到数学问题是怎样被一点点推进的。

这个价值在AI时代尤其重要。因为AI生成结果更容易遮蔽过程，而学习数学恰恰需要看到过程。

6.3 它的问题是无法规模化

Polymath项目需要有人处理大量评论、筛选有效贡献、维护讨论秩序、追踪任务进展。早期工具主要是博客和维基，缺少GitHub、持续集成、现代任务管理和版本控制。

所以它给出的启发很清楚：大规模协作可行，但必须有更好的技术基础设施和管理机制。

7. 形式化项目是Polymath的现代版本

7.1 Lean、GitHub和持续集成改变了协作方式

现代形式化项目可以把大定理分解成很多小引理，不同人认领不同部分，通过GitHub管理任务，通过Lean验证代码，通过持续集成自动检查。这样就比早期博客评论有条理得多。

这类项目的协作模式和Polymath有相似处，但技术条件更成熟。验证可以自动化，任务可以分配，讨论可以被搜索，贡献可以被版本管理。

7.2 AI可以处理局部任务

当一个大定理被拆成许多小任务，人可以把某个引理交给AI尝试形式化。AI可能完成证明，也可能发现命题表述有问题，甚至找到反例。遇到这类问题时，人类仍然要回到社区讨论，修改定义或调整整体结构。

这说明AI适合处理范围清晰的局部任务，但目前还不适合完全接管整体协调。

8. 自主AI代理和人类项目之间的融合困难

8.1 代理可以完成项目，却难以融入项目

现在技术已经可以让自主代理尝试形式化整篇论文。它们可能在技术上成功，但整合到已有形式化项目时会出现很多问题：拆分方式不同，代码风格不同，抽象层级不同，重复证明类似命题，缺少可复用引理。

这类问题不是简单的编译错误，而是工程结构和数学组织问题。形式化代码通过了，不代表它适合进入公共数学库。

8.2 当前基础设施主要为人类设计

论坛、GitHub、Zulip、讨论区、项目管理工具，都是以人为中心设计的。AI代理遇到问题时，不能自然地进入讨论、理解上下文、协商修改方案。于是人类协作流和AI自主流基本分离，只能在微观层面结合：人领一个任务，私下用AI做完，再把结果带回团队。

真正需要的是能让人类和AI共同工作的基础设施，而不是让AI在旁边单独跑。

9. 两类形式化任务必须分开

9.1 第一类：只验证真假

有些项目唯一目标就是确认某件事为真。代码丑不丑、证明好不好读、能不能复用，都不重要。只要形式化系统给出验证通过的结果，就完成任务。

这类任务非常适合AI。可以大量生成、批量尝试、快速筛选，目标清晰，评价标准单一。

9.2 第二类：构建可用的数学知识

另一类项目不只是要形式化一个定理，还要让证明优雅、可读、可复用、能融入已有代码库，能帮助人理解结构。

这类任务不能让AI自由发挥到失控。AI可以做局部子任务，但整体协调、抽象设计、命名规范、证明结构和教学价值，需要人类负责。

10. 激励机制会成为大问题

10.1 数学系统奖励第一个完成的人

当前数学社会系统很看重第一个证明、第一篇论文、第一次形式化。如果AI先生成一个庞大、混乱、难以理解的证明，那么规范化、简化、解释、重构的人反而很难获得同等认可。

这会制造悖论：AI更快完成显性目标，却削弱了人们继续完成隐性目标的动力。

10.2 需要奖励消化、重构和解释

如果一个百万行形式化库证明了某个重大定理，但结构混乱，没有解释，那么它只告诉我们结果成立。真正有价值的工作还包括找出关键步骤、模块化证明、提炼概念、连接文献、写成可教学的版本。

未来数学评价体系需要承认这些工作，不然大家都会追逐第一个验证标记，而没人愿意修路、写地图、建教材。

11. 传统流程会继续存在，但要承认它的速度有限

11.1 人类主导流程不会消失

传统数学流程仍然有价值。它适合深度理解、教学、证明消化、理论整理和共同体训练。它不会因为AI出现就立刻消失。

但它的速度有限。人类阅读、审稿、讲解、学习的速度不会因为AI生成更多结果而同步提高。

11.2 新挑战应该另起一套玩法

除了改造传统流程，还可以设计AI原生的数学挑战。比如让AI在有限预算下处理大量小问题，提交证明或反证，或者参与第一证明类挑战。

这类挑战可以释放AI的能力，又不必强行塞进传统论文系统。传统系统保留理解和教学，新系统负责探索高通量数学实验。

12. 方程理论项目：可扩展数学实验的样本

12.1 数百万个微观定理

陶哲轩提到自己启动过方程理论项目，目标是通过众包和自动化方式证明大量微观定理。这个项目被设计成模块化、可基准测试、适合比较不同方法。

这种问题和传统猜想不同。它不是围绕一个大定理慢慢攻坚，而是把大量小命题组织成可计算、可协作、可统计的任务空间。

12.2 适合AI、人类和混合方法共同推进

这类项目可以容纳人工证明、AI证明、混合证明，也可以用排行榜和基准衡量进展。它更像数学里的高通量实验平台。人类不必逐个手工处理所有问题，而是负责设计问题空间、评估结果、总结结构。

这可能代表AI时代的一种新数学类型：不是只追求单个定理，而是构造一个能持续产生问题、证据、模式和方法的系统。

13. 数学教育和学生训练也要变化

13.1 学生需要看到问题如何被解决

如果AI只交出最终证明，学生看到的是结果，不是思考过程。数学训练依赖失败路线、错误尝试、关键转折和方法选择。Polymath项目的开放过程正好补上了传统论文缺少的部分。

未来好的数学工作流，应该保留过程材料。哪些路线失败了，为什么失败，哪些引理是关键，哪些技术可迁移，这些都应该成为可学习的内容。

13.2 AI不能替代讲解者

一个证明是否进入数学共同体，关键不是它有没有被机器验证，而是有没有人能讲清楚。讲解者需要知道背景、动机、结构、难点和后续方向。

所以AI时代的数学教育，不应只训练学生使用工具，还要训练他们判断、重构、解释和组织证明。

14. 期刊、教材和课程需要重新定位

14.1 期刊不能只筛正确性

在证明泛滥的环境里，期刊如果只关心结果是否正确，会被大量AI产物淹没。正确性可以部分交给形式化验证，但重要性、清晰度、文献关系和可用性仍然需要新的评价机制。

14.2 教材和课程承担证明消化功能

课程和教材会变得更重要。它们不是简单传播已有结论，而是把混乱成果变成可理解结构。未来数学共同体可能更需要高质量阐释者、整理者和架构者。

15. 最核心的判断：AI数学要从产出证明转向组织理解

整场讨论的中心不是AI会不会做数学，而是数学共同体如何吸收AI带来的能力。只要AI产生的证明无法被理解、讲解、复用、整合，它就只是一个孤立结果。真正有价值的新工作流，要让AI的速度和人类的理解能力衔接起来。

可以把问题压缩成一句话：未来数学不缺更快的证明机器，缺的是能把证明变成知识的道路系统。