主题演讲

陶哲轩：AI 时代的数学

Terence Tao - Mathematics in the Age of AI

主题演讲🎤 陶哲轩 (Terence Tao)⏱ 16:34👁 NA

▶ 在 YouTube 观看

陶哲轩讲述数学这一最保守学科如何借助形式化验证、大规模协作与 AI 开始转型，并以「方程理论项目」和与 DeepMind 的合作为例说明 AI 的正确用法。

核心要点

数学是最保守的学科之一：实践数百年几乎未变（柯西 200 年前的教材今天仍可直接使用），且协作程度远低于其他科学（平均每篇论文仅约 2.5 位作者，而其他学科正爆发式增长）。
数学难以大规模协作的根源是系统性的：门槛高（往往需博士才能读懂问题）、证明必须 100% 正确（一处出错就毁掉整个证明）、传统黑板工作流无法扩展到上百人。
形式化验证 (formal verification) 是让新工作流跑通的「秘密配方」：用 Lean 等证明助手自动检查论证对错，过滤掉大量错误，从而打破信任壁垒、可接受匿名/不可信的贡献。
「方程理论项目」证明了大规模协作的可行性：约 50 位多为非专业的合作者，在 3 个月内对 2200 万个代数蕴含问题全部给出证明或反证。
当前 LLM 不可靠（连简单算术都会出错），但与验证器结合并形成「生成—检查—纠错」的循环后才真正有用；与 DeepMind 合作的 AlphaEvolve 已在装箱等优化问题上刷新了数值记录。
AI 最有价值的用法不是替代数学家攻克难题，而是「扩大蛋糕」：用 AI 批量处理中等难度问题的长尾、摘取低垂果实，把真正困难的部分上交给人类专家。

分章详解

数学：一门拥抱变化最慢的学科

以柯西 200 年前介绍柯西积分公式的教材为例：除了语言是法语、未用现代排版，内容几乎与今天给研究生的教材相同。
数学的「连续性」是其巨大优势——会沿用 200 年甚至 2000 年前的结果（如日常使用毕达哥拉斯定理），但也导致其不愿追逐潮流。
数学家几乎是唯一仍坚持黑板与粉笔的学科（陶哲轩自己办公室就有六块黑板），其他学科早已转向 PPT 和白板；摄影师 Jessica Wynne 还为数学家的黑板出了影集。

为什么数学家不善于大规模协作

科学计量显示数学论文平均作者数从约 1.5 缓慢升到 2.5，而其他科学正拥抱大型协作项目、蓬勃发展。
三大系统性障碍：入门门槛高（常需数学博士才能理解问题）；要求每个细节 100% 正确，众包时一个错误就摧毁整个证明；黑板式工作流无法扩展到互联网上的上百人。
数学正从「个案研究」（一个问题做几个月、出一份报告）转向「普查」式研究（一次研究成百上千个问题，报告统计规律），并开始出现「公民数学」。

案例一：方程理论项目 (Equational Theories Project)

去年在 UCLA 发起，约 50 位合作者多为计算机科学家、研究生、本科生甚至高中生，多数素未谋面。
程序化生成了 2200 万个代数问题（典型形式：交换律是否蕴含结合律？答案为否），单题虽可由研究生花一小时解决，但 2200 万题无法靠人力或单纯众包完成。
团队在 3 个月内对全部问题给出证明或反证：用 GitHub 存放并用 Lean 统一形式化以自动验证，用 Zulip 讨论板让人写证明、计算机程序批量攻击（一次可处理约 10 万题），人证明与机器证明反复互转。
成功要素：高度模块化（可认领子集、可专精于写人类证明或翻译成机器证明）；有良好的度量/损失函数（如第 16 天 2200 万题仅剩 888 题未解，人人努力把这个数字往下推）；可去中心化、自发协作。
形式化验证打破信任壁垒：贡献无需逐行检查或依赖声誉即可接纳；还能进行原子级精确讨论，例如九步证明中第八步通过、唯一卡住的微步骤可被精确指明并讨论。

案例一点五：与 Google DeepMind 的合作 (AlphaEvolve)

正在与 DeepMind 合作但论文尚在审批中，只能讲大方向：LLM 日益强大（能解奥赛题、有时能答深层数学问题），但会犯低级错误（演示中把 7×4+8×8 算错，被指出后才更正）。
把不可靠的 LLM 输出与「验证器」结合才可能有用：让 LLM 生成、测试、把报错回传让其纠错，形成循环。
他们的工具 AlphaEvolve（底层含演化/遗传算法）通过让 LLM 随机尝试、获取反馈、演化代码，已在装箱类问题上取得数值改进（如用 11 个六边形求能容纳它们的最小六边形）。
这些有限维优化只是测试案例，是全部数学问题的极小子类；他们在无限维优化上已有新进展，论文几周内将发布。

AI 在数学中的现实用法与未来

已实际可用的场景：写代码大幅变易、文献综述、把数据喂给 AI 得到新猜想或发现新模式（仍是零散概念验证、尚不能系统化）、作为跨学科/对公众的「通用翻译器」打通术语隔阂。
要走向更高级应用，必须依赖严格验证来过滤——只能信任或可核查到的范围内使用 AI，否则风险太大。
AI 帮助单个数学家有限，融入更广泛协作、填补缺口时最有效；最佳定位不是与人争夺现有工作，而是『扩大蛋糕』，让更多目标在经济上变得可行。
总体而言应用前景广阔但极度情境化：不是即插即用，必须懂得何时用、如何用。

关键引述

“这是一个变化与不确定的时代，而这正是我所在的领域不太习惯的——我们大概是对待变化最保守的学科之一。”— 陶哲轩 (Terence Tao)

“形式化验证打破了信任壁垒：我们能接受来自素未谋面的人、不被信任的匿名贡献，因为它们都必须通过自动验证。”— 陶哲轩 (Terence Tao)

“AI 不应与人类已有的工作去争抢同一块蛋糕，而应把蛋糕做大、创造更多新任务。”— 陶哲轩 (Terence Tao)

术语 / 人物

形式化验证 (formal verification) — 一类计算机语言技术，可将数学论证自动检查是否正确，是大规模协作得以成立的关键，能过滤错误并打破信任壁垒。

Lean — 本项目采用的证明助手语言，用于把人工与机器生成的证明统一形式化，从而自动验证其正确性。

方程理论项目 (Equational Theories Project) — 陶哲轩在 UCLA 发起的开放协作项目，约 50 人在 3 个月内对程序生成的约 2200 万个代数（magma 等式律）蕴含关系全部给出证明或反证。

自动定理证明器 (automated theorem provers) — 一类『传统 AI』工具（如 Vampire），在本项目核心任务上的表现优于现代 LLM，是机器证明的主力。

AlphaEvolve — DeepMind 的工具，底层含演化/遗传算法，通过 LLM 生成、反馈、演化代码来求解优化问题，已在装箱等问题上刷新数值记录。

magma（广群/原群） — 一种只带单个二元运算、无其他约束的代数结构；项目研究的就是其上各等式律之间的相互蕴含关系。

背景补充

陶哲轩 (Terence Tao) 是 UCLA 数学教授、菲尔兹奖得主，被誉为当代最杰出的数学家之一，也是 SAIR（科学与 AI 研究基金会）的联合创立者。他于 2024 年 9 月发起「方程理论项目」，联合专业与业余数学家、自动定理证明器和 Lean，研究约 4694 条 magma 等式律之间的蕴含图（约 2200 万个有序对），项目论文于 2025 年 12 月发布。其中 LLM 主要用于辅助（如用 Copilot 加速写 Lean 证明、用 Claude 协助写可视化代码），核心求解则由 Vampire 等传统自动定理证明器完成。他另与 DeepMind 及 Javier Gómez-Serrano 合作，用 AlphaEvolve、AlphaProof、Gemini Deep Think 推进数学研究，包括为有限域 Kakeya 猜想发现新构造。

适合谁看

关注 AI 与数学/科研结合的研究者、数学与计算机专业学生、对开放协作与形式化证明感兴趣的开发者，以及希望了解 AI 如何真正落地于严肃科研的科技从业者与决策者。