2023 年 10 月，菲尔兹奖得主陶哲轩（Terry Tao）在社交媒体上宣布开始学习 Lean 4 交互式证明系统，并明确提到 "必要时使用 AI 辅助"。这一举动标志着一位顶尖数学家正式将大型语言模型与形式化验证工具纳入其研究 workflow。不同于泛泛讨论 AI 潜力的学者，陶哲轩在过去两年间主导了多个高可见度的形式化项目，构建出一套可复现的人机协作验证流程。
从 Maclaurin 不等式到 PFR 猜想的形式化实践
陶哲轩的 Lean 学习路径遵循 "由小到大" 的渐进策略。首个实验是将一篇仅 10 页的 Maclaurin 不等式证明形式化。他在实践中发现了一个反直觉的现象：证明中 "困难的部分在 Lean 里很容易形式化，而简单的部分反而耗费大量时间"。例如，证明三个大于 1 的数之和至少为 3 这一显然事实，在 Lean 中需要显式引用 Mathlib 库中的引理；而数字 "3" 在不同数域（自然数、整数、实数）中的类型声明也必须精确指定，否则会导致编译失败。
这一经验为后续更大规模的项目奠定了基础。2023 年 11 月，陶哲轩与 Ben Green、Timothy Gowers（同为菲尔兹奖得主）及 Freddie Manners 合作完成了多项式 Freiman-Ruzsa（PFR）猜想的形式化。该项目从启动到完成仅用时三周，参与者在 Lean 社区聊天频道中协调分工，将证明拆解为 13 个主要章节，每个章节进一步细分为约 5 行代码的小型引理。这种极度模块化的分解策略使得数十名贡献者能够并行工作，而 Lean 的自动验证机制则消除了传统 Polymath 项目中人工审核的瓶颈。
模块化分解与人机分工的工程化框架
陶哲轩方法论的核心在于将复杂数学证明转化为可并行处理的子任务网络。在 PFR 项目中，他将原本需要连续推理的证明链条打断，转化为数百个独立的引理声明，每个引理都有明确的输入输出规格。这种设计使得贡献者无需理解整个证明的全貌，只需专注于自己认领的局部任务。
人机分工遵循 "AI 处理规模，人类处理深度" 的原则。陶哲轩观察到，当前大语言模型在数学前沿领域的表现 "像过度自信的大学生"—— 能够提出看似合理的建议，但缺乏区分好坏想法的专业判断力。因此，AI 被部署在子问题生成、代码补全和简单引理搜索等任务上，而核心证明策略、关键引理的设计以及最终验证仍然由人类数学家主导。
形式化验证系统在此扮演了 "真理机器" 的角色。Lean 不仅检查每一步推导的逻辑正确性，还强制要求所有数学对象都有明确的类型定义。这种严格性在初期增加了工作量，但换来了可复现性和错误免疫能力 —— 一旦通过 Lean 验证，证明的正确性不再依赖于审稿人的主观判断。
规模验证：Equational Theories 项目的压力测试
2024 年 9 月，陶哲轩发起了 Equational Theories 项目，这是对其方法论的一次大规模压力测试。该项目旨在绘制涉及 4,694 个代数定律的完整蕴含关系图谱，共计约 2,200 万条潜在逻辑蕴含需要验证或证伪。
项目启动后 48 小时内，参与者使用 Python 脚本对简单结构（magmas）进行测试，解决了超过 99% 的蕴含关系。剩余 238 个复杂案例则交由自动定理证明器和人类数学家处理。到 2024 年 11 月，未解决问题缩减至 138 个；2025 年 3 月，仅剩 4 个蕴含关系悬而未决。这种 "快速收敛" 现象验证了陶哲轩的假设：将问题分解为数千个小型子任务后，AI 辅助的大规模协作能够以远超传统模式的速度推进。
更具意外收获的是，该项目在探索过程中发现了 "magma cohomology" 这一全新数学构造 —— 这是群上同调理论的一个变体，此前未被文献记录。陶哲轩向该领域专家 John Baez 求证后确认这是一个新发现。这一案例表明，形式化探索不仅是验证工具，也可能成为数学发现的来源。
AI 数学能力的边界评估与协作模式
陶哲轩对 AI 在数学研究中的定位持审慎乐观态度。他认为，当前大语言模型在两类场景中表现最佳：一是存在大量训练数据的常规问题求解，二是可被分解为数千个小型子任务的复杂问题。在前沿数学领域（训练数据稀少的区域），AI 的可靠性显著下降。
他提出的协作模式包含三个关键组件：人类洞察负责战略方向和创新突破，AI 负责规模化的子问题求解和代码生成，形式化验证系统负责 correctness guarantee。这一三角架构试图平衡效率与可靠性 ——AI 提升吞吐量的同时，Lean 确保输出质量。
对于希望引入类似流程的研究团队，陶哲轩的实践提供了可落地的参考参数：将证明模块化为 5-20 行代码的引理单元；使用 GitHub Copilot 等工具辅助 Lean 代码生成；通过 Zulip 等实时协作平台协调分布式贡献者；利用 Mathlib 等现有形式化库减少重复劳动。同时他也坦承当前形式的局限：年轻数学家参与形式化工作难以获得传统学术评价体系的认可，这一激励机制问题仍需解决。
陶哲轩的 evangelism 并非宣扬 AI 将取代数学家，而是展示一种 "实验数学" 的新范式 —— 类似于物理学中理论与实验的分工协作，数学研究也可能分化出专注于形式化验证和计算实验的新分支。这种范式转变是否会被更广泛地接受，取决于工具链的成熟度和学术评价体系的适应性调整。
资料来源
- Kevin Hartnett, "How Terry Tao Became an Evangelist for AI in Math", Quanta Magazine, 2026-06-08
- Terence Tao et al., "On a conjecture of Marton", arXiv:2311.05762, 2023
内容声明：本文无广告投放、无付费植入。
如有事实性问题，欢迎发送勘误至 i@hotdrydog.com。