陶哲轩提出 Math 2.0：AI 打破证明稀缺性，数学研究范式转向可验证性与想象力重构Hacker News AIT2基座大模型

Hacker News AI · 2026/10/11 21:16:45

陶哲轩提出 Math 2.0：AI 打破证明稀缺性，数学研究范式转向可验证性与想象力重构

原标题：Terence Tao: Math 2.0 [pdf]

78AI 研判分

核心综述

菲尔兹奖得主陶哲轩发表演讲阐述“Math 2.0”概念，指出 AI 正在颠覆传统数学研究中基于“证明稀缺性”的旧范式。他强调，由于数学证明具备独特的客观可机械验证属性，AI 能高效生成并校验证明，从而将人类的核心价值从寻找解法转移至定义问题与发挥想象力。这一观点为 AI 时代数学研究的职业定位与方法论提供了新的理论框架。

报道全文原始报道全文

本文目录20 个章节

AI 对数学的颠覆

现代 AI 工具的出现正在颠覆许多长期稳定的职业。

我所在的数学研究领域——在过去近一个世纪里基本保持稳定——已被证明极易受到此类颠覆的影响。

证明稀缺的历史时代

传统数学（或称“Math 1.0”）是在“证明稀缺”的假设下运作的。

找到一个开放数学问题的解（并证明其正确性）既困难又罕见，往往需要大量的人类专业知识才能完成。

Math 1.0 的许多机构、传统、激励机制和既定目标都是基于这一“证明稀缺”假设组织起来的。

客观可验证性

另一方面，证明具有一种在其他大多数学科中罕见的特性：客观可验证性。

不同的数学家可能对哪些类型的数学有趣或富有成果存在分歧。

但对于什么构成给定问题的正确且完整的证明，存在着广泛的共识。

事实上，如果证明是用适当的证明助手语言（例如 Lean）编写的，甚至可以通过计算机机械地检查证明。

数字化与高质量数据

证明还具有高度数字化的特性；它们不需要物理实例化，不需要真实世界的数据作为输入，也不需要真实世界的实验来验证输出。

原则上，仅使用标准数学教科书或库提供定义，就可以通过纸笔生成并验证证明。

解决复杂的数学问题通常还需要了解相关的研究文献；但如今，海量的这类文献已以数字形式可用。

证明丰裕的时代

客观可验证性、数字化以及大规模高质量数据集的结合，使得解决数学问题的任务特别适用于驱动现代 AI 的机器学习技术。

因此，前沿 AI 实验室优先推进数学问题解决能力的进步，领先于那些缺乏上述三个特征之一或多个的其他应用。

由于这种巨额投资，我们现在正进入数学中的“证明丰裕”时代。

AI 参差不齐的能力

在算力充足且能访问前沿 AI 模型的情况下，人们现在可以在相对较短的时间内获得许多此前被认为难以解决的开放问题的解。

越来越多的情况下，用户无需具备特殊专业知识即可通过提示 AI 获得此类解决方案。

这与当前 AI 在主观性强、依赖现实世界交互或数据稀缺的任务上的表现形成了鲜明对比。

因此，AI 的性能呈现出极度的“锯齿状”特征：在某些方向上令人惊叹，而在其他方面却显得不足。这一现象不仅存在于数学领域，在更广泛的范围内也是如此。

数学的新前沿

尽管新闻稿和社交媒体给人留下了某种印象，但即使投入巨大的计算资源，当前数学前沿的大部分问题仍未得到解决。

事实上，数学问题的空间是无限的；这些问题的难度水平也是没有上限的。

正因如此，未来的数学前沿将始终持续扩展。

将目标与数学的长期健康对齐

此外，虽然问题解决历来是研究性数学中最显眼的目标之一，但它只是更具价值的长期目标的一个代理指标。

在证明稀缺的时代，这个代理指标大体上是准确的，但在证明丰富的时代，它已变得错位。

如今，单纯盲目地优化问题解决能力实际上正在损害数学的长期健康。数学的未来——“Math 2.0”——既需要拓展研究前沿，同时也需要将传统的问题解决角色去中心化。

报告偏差

哇，我在社交媒体上看到的所有数学问题都被 AI 解决了！

我们迫切需要更透明、更科学的 AI 能力评估，全面报告关键统计数据，如资源消耗和负面结果。

First Proof ( https://1stproof.org/ ) 就是朝此方向努力的一项尝试。

数学的前沿

所有数学任务

· · · · · · · · · · · · · · ·

......人类 + AI 人类 AI

当前的新闻稿和社交媒体活动更具想象力和创造力的 AI 应用 Math 1.0 研究前沿 Math 2.0 研究前沿未报告的 AI 失败尝试

一旦我们更具想象力地采用 AI，数学的研究前沿将显著扩展。

实验数学的新纪元

我们现在有能力收集过去无法生成或极不切实际的大规模数学数据集。

早期的例子包括“等式理论项目”（Equational Theories Project）和 SAIR/LMFDB 逆伽罗瓦问题挑战。

有了这些数据集，我们可以进行新型的实验数学：从“个案研究”转向“群体调查”。

这将有助于描绘出研究前沿新的“难度景观”，随着强大 AI 工具的可用，这一景观的形态已发生显著变化。

等式理论项目 (2024–2025)

ETP 众包了人类和自动化的论证过程，以解决泛代数中超过 2200 万个真/假命题。

逆伽罗瓦问题挑战 (2026)

IGP24 的第一阶段是一场成功的众包竞赛，旨在为每个该次数下可能的 25,000 个伽罗瓦群找到对应的 24 次多项式。第二阶段将是一项协作努力，旨在将范围扩展至 31 次。

超越问题解决

与普遍观点（或我们某些营销宣传）相反，数学家并非仅仅专注于解决未决问题。

特别是在纯数学领域，未决问题充当着“灯塔”的角色：它们本身并非要抵达的目的地，而是探索这些问题周围数学景观的有用指南。

在尝试解决这些问题过程中学到的经验——无论结果是成功、失败还是取得部分进展——往往比问题的最终解决方案更有价值。

通过自动化工具过早地抵达这些灯塔，可能会破坏对未选择路径的探索，并使周边领域变得贫瘠。

关于问题解决的朴素观点

AI 出现之前：

数学问题 → 数学解答

AI 出现之后：

数学问题 → 数学解答 ← AI

这难道不是一件好事吗？

更准确的模型

应用数学问题 → 对齐的应用数学解答 / 未对齐的应用数学解答纯数学问题 → 纯数学解答 → 人类理解

“Math 1.0”问题解决“生态系统”的简化视图。未决问题在一个可再生的循环中被解决；而从解决纯数学问题中获得的见解可以安全地转移到应用问题上。

应用数学问题对齐的应用数学解法未对齐的应用数学解法 AI 人类理解纯数学问题纯数学解法

不加区分地使用 AI 以不可持续的方式解决问题，会损害该领域的长期健康与发展，也会阻碍其向更复杂、更混乱的现实世界应用的安全迁移。

关于对齐与理解的思想实验

假设一个高级 AI 被提示“寻找一种能通过 III 期临床试验的癌症疗法”。

经过大量计算后，它产生了一种由未知化学物质组成的混合物，其数学模型预测，当这种混合物注入患者体内时，将杀死所有癌细胞。

虽然没有人真正知道这种混合物是如何被发现的，但该模型的预测已在 Lean 中得到验证，且这种混合物确实通过了 III 期临床试验。

AI 针对该提示的解决方案是否可能通过利用试验过程中的弱点而变得未对齐？

在将这种混合物注入你的血液之前，你是否希望至少有一位人类癌症专家理解这种疗法的机制？

或者，是否希望有一位人类数学家理解用于定位这种混合物的数学模型？

应用数学问题对齐的应用数学解法未对齐的应用数学解法人类理解纯数学问题纯数学解法

+AI +AI +AI +AI

更具可持续性的“Math 2.0”式 AI 用法，应当是加强人类理解与数学交互的所有方式。

“Math 2.0”式 AI 用法的示例

“开放式阐释问题”而非开放式研究问题：为那些已知证明目前晦涩难懂的结果寻找有动机的解释。（新修订的 Caltech Mathathon 就是这一方向上一个有趣的实验。）

将许多研究论文汇编成一个更大的动态网络。（Integrated Explicit Analytic Number Theory Network 就是构建此类网络的初步尝试。）

创建大规模、高质量的正式数学库，例如 Mathlib。

使用 AI 来发现并突出新的原理、方法或见解，而不仅仅是新的证明。

Maththon（11 月 13-15 日）是一场由学生主导的活动，旨在利用开源 AI 工具，为现有结果寻找新的或改进的证明——这些结果的当前证明在某些方面存在不足。

集成显式解析数论网络（IEANTN）。IEANTN 是一个动态的“电子表格”，它整合了显式解析数论中大量相互关联的结果，可以通过向网络中添加或移除结果来实时更新。