AI for Mathematics：当人工智能邂逅纯数学——2026年的突破性进展

引言

当 David Hilbert 在 1920 年代提出他的宏伟计划——将所有数学形式化，在一致的公理系统内证明每一个定理时，他可能无法想象，一个世纪后的今天，人工智能正在将这个梦想逐步变为现实。

2026 年 2 月，北京大学的 Ju 和 Dong 在 arXiv 上发表了一篇重要的综述论文：“AI for Mathematics: Progress, Challenges, and Prospects”。这篇论文系统地梳理了人工智能在数学领域的最新进展，展示了 AI 如何从一个计算工具转变为数学研究的真正合作者。

AI 邂逅纯数学，正在开启数学研究的黄金时代！

AI for Mathematics 的两大方向

论文将 AI for Mathematics（AI4Math）的研究分为两个互补的方向：

1. 问题特定建模（Problem-Specific Modeling）

这种方法针对特定的数学问题设计专门的架构。它的优势在于：

针对性强，效果显著
数据和计算资源需求较少
更易被广大研究者使用

但缺点是：

难以迁移到其他领域
需要大量的领域专业知识

2. 通用建模（General-Purpose Modeling）

这种方法专注于开发基础模型，从数学专用的语言模型到通用推理引擎。它的优势在于：

通用性强，可跨领域应用
支持更广泛的工作流

但缺点是：

需要海量训练数据
计算资源需求巨大
工程复杂度高

令人惊叹的突破性成果

1. 引导人类直觉

AI 已经能够帮助数学家发现隐藏在高维数据中的模式，从而提出新的猜想。

最著名的例子是 2021 年 DeepMind 的工作，他们使用神经网络发现了纽结理论中代数和几何不变量之间的新关系，并提出了对称群组合不变性猜想的候选算法。

最近，AI 还在仿射 Deligne-Lusztig 簇的研究中独立重新发现了经典的虚维数公式，并建立了新的精确下界定理。

2. 构造例子和反例

AI 正在帮助数学家构造反例，以验证或反驳数学猜想。这可是数学研究的”黑科技”！

FunSearch（2024）：使用进化方法搜索生成所需构造的程序，发现了超越之前已知结果的大型 cap 集构造。
AlphaEvolve（2025）：使用更强的 LLM，将进化过程扩展到整个代码文件，并同时优化多个指标。它为最小重叠问题和 11 维接吻数问题等提供了改进的构造。

3. 形式化推理：从 IMO 到研究前沿

这是最令人兴奋的领域！AI 正在掌握形式化数学推理的艺术，这可是数学界的”王炸”！

AlphaGeometry 系列

AlphaGeometry（2024）：将符号几何推理引擎与语言模型结合，达到了 IMO 银牌得主的水平。
AlphaGeometry2（2025）：进一步扩展了形式几何语言，引入了共享知识集成搜索树（SKEST）算法，实现了 IMO 金牌得主的表现。

定理证明的 Agent 时代

最近的进展已经从单一模型转向模块化的 Agent 工作流：

Draft, Sketch, Prove（DSP）：生成非形式化证明，将其翻译为带有开放子目标的形式化草图，然后使用轻量级证明器关闭这些子目标。
LEGO-Prover：维护一个持久的引理库，通过维度扩展、关键概念识别、参数化和复杂度增强等策略将已验证的引理演化为新引理。
Aristotle：将非形式化推理与形式化验证交错进行。它将证明草拟为引理序列，将其形式化，并尝试验证，根据反馈迭代改进其输出。与几何求解器结合，它达到了 IMO 金牌得主的水平。
Numina-Lean-Agent（2026）：为 Claude Code 配备 Lean-LSP-MCP 来与 Lean 交互、用于定理检索的语义搜索引擎、非形式化证明器和外部 LLM。它成功解决了 2025 年 Putnam 竞赛的所有问题！

4. 在 Erdős 问题上的突破

最令人震惊的是，在 2025 年末和 2026 年初，像 Aristotle 这样的 Agent 系统已经成为 Terence Tao 等人研究 Paul Erdős 猜想的高杠杆验证工作流的组成部分。

这个工作流是这样的：

前沿语言模型（如 Gemini Deep Think、ChatGPT）生成候选构造或启发式论证
这些论证在 Lean 中被严格形式化和机械检查

这个管道已经产生了对几个 Erdős 问题（特别是问题 #205）的形式化验证反例，以及对更复杂问题（如 #367）的部分解决！

性能评估：从竞赛到研究生水平

论文中提供了令人印象深刻的性能数据：

北京大学本科期末考试

在 11 个本科数学科目的期末考试中：

GPT-4：得分低于 60 分
推理增强模型（OpenAI o 系列、DeepSeek-R1、Gemini 2.5 Pro）：显著提升，多个超过 90 分

北京大学博士资格考试

在分析、概率、代数和几何与拓扑四个领域的博士资格考试中：

o3-mini：平均得分 84.4 分
模型在代数方面表现最强，在几何与拓扑方面得分最低

这表明当前的 AI 系统在处理抽象代数结构方面比需要几何直觉的任务相对更擅长。

数学信息检索：寻找”针海中的针”

随着数学库的增长（如 mathlib4 现在包含超过 250,000 个定理和 120,000 个定义），有效地检索相关定理成为了主要瓶颈。

论文中讨论了几种关键的检索任务：

前提检索：识别可用于证明新定理的有用定理、引理或定义
语义检索：基于含义识别数学上等价或密切相关的陈述
问答检索：响应对数学答案、解释或支持性文档的自然语言查询

像 LeanSearch、Moogle、LeanExplore、LeanFinder 和 LeanDex 这样的工具正在使数学家能够更有效地在大型数学库中导航。

挑战与未来方向

尽管取得了令人印象深刻的进展，论文也指出了几个关键挑战：

1. 领域专业知识和特征工程

在问题特定建模中，输入特征的设计通常需要深厚的领域专业知识。人类直觉对于选择数学上有意义的特征和解释模型输出来推导出理论见解仍然不可或缺。

2. 验证瓶颈和自动形式化

准确高效的验证构成了研究水平数学的关键瓶颈。自然语言的固有歧义，加上能够审计高级证明的专家稀缺，使得手动验证缓慢且容易出错。

3. 形式化中的语义一致性

自动形式化中的一个微妙挑战是验证生成的形式化陈述的语义正确性——即形式化陈述是否忠实反映了原始非形式化陈述的意图。

4. 超越正确性到理解

形式有效性是数学价值的必要条件，但不是充分条件。正如 William Thurston 所说：”数学不是关于数字、方程、计算或算法：它是关于理解。”

5. 从启发式到专家例程

虽然独立的 LLM 作为强大的推理引擎，但 AI4Math 的未来在于设计用于模拟专业数学家复杂工作流的 Agent 系统。

6. 积极的社区参与

AI 推理的进步需要数学家的积极干预。除了生成形式化数据外，社区还必须积极探索这些系统，以发展它们能力和边界的集体”心理模型”。

7. 拥抱 AI 辅助研究

我们必须为文化转变做好准备，AI 从计算工具演变为研究副驾驶。2025 年末的发展强调了这种转变。在这项工作中，作者观察到，虽然这些模型可能仍然缺乏真正的理解，经常”模仿思考”，但它们已经擅长自主发现逃避人类直觉的数学构造。

结论

这篇论文描绘了 AI for Mathematics 领域令人振奋的图景。从引导人类直觉发现新的数学关系，到构造反例验证猜想，再到掌握形式化推理达到 IMO 金牌水平，AI 正在成为数学研究不可或缺的工具。

最令人兴奋的是，我们正在见证一个范式转变：AI 不再仅仅是验证已知结果的工具，而是正在成为积极探索未知数学领域的合作者。

正如论文作者所指出的，真正的价值在于：

“一个有价值的证明不仅仅是建立真理；它提供了见解，揭示了结构，并提供了适用于其他问题的技术。”

未来的 AI 系统不仅要验证数学真理，还要帮助我们发现那些重塑我们思维、揭示之前看不见的联系的证明。在人工智能的辅助下，数学研究正在进入一个新的黄金时代。

论文信息：

标题：AI for Mathematics: Progress, Challenges, and Prospects
作者：Haocheng Ju, Bin Dong
机构：北京大学
日期：2026年2月9日
arXiv：2601.13209