摘要：2024年是AI数学推理的”iPhone时刻”。AlphaProof在IMO 2024上获得银牌，AlphaGeometry在几何领域超越人类金牌水平，DeepSeek系列开源模型将形式化证明的入门门槛降到几乎为零。本文系统梳理了这场正在发生的”AI数学革命”的技术脉络：从神经符号方法到强化学习证明搜索，从Lean社区爆发到AI辅助数学家的工作流变革，并给出我对”AI是否会取代数学家”的判断。

一、2024：AI数学推理的”iPhone时刻”

2024年7月，伦敦的IMO（国际数学奥林匹克）赛场上传来了一个让数学界和AI界同时震动的消息：Google DeepMind的AlphaProof系统在IMO 2024中获得了银牌水平（4/6题满分，总分28/42），而它的”姐妹系统”AlphaGeometry 2在几何题上获得满分。

这是AI首次在IMO上达到人类竞赛选手的奖牌水平。如果将时间倒推两年——2022年，最好的AI数学系统在IMO上的得分是0——这个跨越的速度令人震惊。

但事情远不止”AI会做题”这么简单。 在这背后，一场更深层的革命正在数学界悄然发生：

  • Lean 形式化证明社区的用户量在 2023-2025 年间增长了约 5 倍
  • DeepSeek-Prover 系列将开源形式化证明的能力推进到本科数学水平
  • 多个数学研究团队开始将 AI辅助证明 纳入日常工作流
  • “形式化数位化” 从一个小众学术活动变成了主流数学期刊的讨论话题

本文将基于公开的论文、技术报告和社区数据，系统梳理这场”AI数学革命”的技术全景。

二、AlphaGeometry：从零开始的几何推理

2.1 核心方法：神经符号合成

2024年1月发表于 Nature 的论文 “Solving olympiad geometry without human demonstrations”（Trinh, Wu, Le, He, Luong）提出了一个神经符号系统，其核心创新在于无需人类演示数据。

组件 类型 作用
神经语言模型 Transformer 从几何图形中提取语义特征，预测辅助点/辅助线的构造
符号演绎引擎 DDoS (专门面向几何的搜索) 基于欧几里得几何的公理系统进行穷举推导
合成数据生成器 自动随机生成 生成 1 亿道不同难度的几何题及其证明路径

合成数据是关键突破：

传统方法需要人类标注的几何题和证明来训练模型。AlphaGeometry 的做法是：

1
2
3
4
5
6
7
随机生成几何构型
    ↓
符号演绎引擎尝试推导所有可导出的结论
    ↓
将"构型 → 结论"对作为训练数据
    ↓
训练神经模型预测"给定构型，下一步该做什么"

这 1 亿道合成题使神经模型学会了在遇到真实 IMO 几何题时如何”灵光一现”——提出生成序贯的辅助线/辅助点构造。

2.2 性能

基准 之前最好 (2022) AlphaGeometry AlphaGeometry 2
IMO 2000-2023 几何题 54% 88% 92%
IMO 2024 几何题 — — 满分
辅助构造路径 需人类示范 零示范 零示范

2.3 局限

AlphaGeometry 仅支持欧几里得平面几何。它不能做数论、组合、代数等问题。它的成功在于 “将几何这个特定领域的形式化做到极致”，而非通用数学推理。

三、AlphaProof：更通用的强化学习方法

3.1 系统架构

AlphaProof 是比 AlphaGeometry 更通用的系统——它使用强化学习 + 形式化语言（Lean） 的组合来处理更广泛的数学问题：

1
2
3
4
5
6
7
8
9
问题陈述（自然语言或形式化）
    ↓
编码器 → 转化为 Lean 形式化表述
    ↓
策略网络（Transformer）→ 预测下一步 tactic
    ↓
Lean 内核验证 → 成功或失败
    ↓
PPO 强化学习更新策略

AlphaProof 在 IMO 2024 上的表现（6 题中 4 题满分）：

题号 领域 AlphaProof 人类金牌线
第1题 数论 ✅ 满分 ✅
第2题 代数 ✅ 满分 ✅
第3题 代数 ✅ 满分 ✅
第4题 组合 ❌ ✅
第5题 几何 ✅ 满分 ✅
第6题 组合 ❌ ⚠️ 仅少数选手完成

3.2 训练方法的技术细节

AlphaProof 的 RL 管线有三个关键设计：

  1. 课程学习（Curriculum Learning）：从简单 IMO 题开始训练，逐步提升难度
  2. 自对弈（Self-Play）：每次生成多个证明候选路径，用 Lean 内核验证，将成功的路径作为正反馈
  3. 搜索时计算扩展：推断时可以用更多计算资源来搜索更深的证明树

这与 AlphaGo 的思路如出一辙：将定理证明视为一种”两人游戏”——证明者 vs 验证者，验证者（Lean 内核）是完美的（不犯错），证明者需要找到通往目标的路径。

3.3 计算成本

AlphaProof 的一个被低估的话题是它的计算开销：据报道，单个 IMO 题的证明搜索可能需要数小时到数天的 GPU 时间。这与人类选手的”90 分钟内完成一题”相比，效率差距巨大。

但重要的是：AlphaProof 不需要人类的数学直觉，它通过暴力搜索+学习来弥补。随着硬件效率提升和模型架构优化，这种差距正在快速缩小。

四、DeepSeek-Prover：开源社区的逆袭

如果说 DeepMind 的 AlphaProof/AlphaGeometry 代表了”闭源巨头”的路线，那么 DeepSeek-Prover 系列（DeepSeek AI，2024-2025）则代表了”开源社区”的力量。

模型 日期 在 Lean 上的表现 开源
DeepSeek-Prover v1 2024.08 MiniF2F 验证集 34.6% ✅
DeepSeek-Prover v2 2025.01 MiniF2F 验证集 41.8% ✅
社区改进版 2025.03 多个团队用 LoRA 微调达 ~45% ✅

DeepSeek 的核心贡献在于开源了训练管线的每一环：

  1. 合成数据生成器：从已有定理自动生成形式和难度各异的训练数据
  2. Lean 环境接口：将 Lean 的 tactic 执行环境封装为可 RL 训练的 gym 环境
  3. 预训练模型权重：可在消费级 GPU（RTX 4090）上微调

这使得全球的研究人员和数学爱好者都能参与进来——到 2025 年底，社区改进版已经追平甚至在某些子集上超越了闭源系统。

开源 vs 闭源的张力

1
2
3
4
5
6
7
                  DeepMind (闭源)          DeepSeek (开源)
                  ─────────────           ─────────────
性能 (MiniF2F)    领先 ~5%                 快速追赶
可复现性           ❌ (未公开完整代码)       ✅ (全部公开)
可定制性           ❌ (黑盒)                ✅ (可微调)
硬件需求           企业级 GPU               消费级 GPU
社区贡献           ❌                       ✅ (全球社区迭代)

五、形式化证明生态：Lean 的爆发

5.1 Lean 是什么

Lean（由微软研究院 Leonardo de Moura 开发）是一个交互式定理证明器（Interactive Theorem Prover, ITP）。它是数学家的”IDE”——你写定理，用 tactic 构造证明，Lean 内核验证每一步的逻辑正确性。

5.2 2023-2025 的增长曲线

指标 2023 年 2025 年 增长
Lean 社区包 (mathlib4) 定理数 ~80,000 ~135,000 1.7x
GitHub 活跃贡献者 ~200 ~800 4x
形式化的本科数学占比 ~40% ~65% —
开设 Lean 课程的高校 ~15 ~60+ 4x

这组数字的驱动力来自两个方向：

  1. “自顶向下”：Fields 奖得主如 Peter Scholze、Kevin Buzzard、Terence Tao 等公开倡导形式化证明，并在自己的研究中实际使用 Lean
  2. “自底向上”：AI 系统（AlphaProof、DeepSeek-Prover）自动生成或辅助生成证明，大幅降低了进入门槛

5.3 典型案例：液体张量实验的形式化

2024 年，Peter Scholze（Fields 2018）提出的”液体张量实验”（Liquid Tensor Experiment）在 Lean 中完成形式化验证。这是一个长达数年的项目，最终由国际团队协作完成，证明了：

“即便是最前沿的数学研究，也可以被形式化验证。”

这个案例的意义远不止一个定理的验证——它展示了分布式形式化证明的工作模式：不同数学家负责不同引理，Lean 的内核确保整体逻辑一致性。

六、未解难题：AI 数学推理的七个局限

尽管 2024-2025 年的进展令人振奋，但我们需要对 AI 的数学能力保持清醒的认识。

6.1 局限清单

局限 说明 是否正在被解决
1. 竞赛 vs 研究 IMO 是”已知答案的封闭问题”，前沿研究是”没人知道答案的开放问题” ❌ 差距巨大
2. 形式化鸿沟 自然语言定理需要先形式化为 Lean 代码，这一步目前需要大量人工 ⚠️ AI辅助翻译中
3. 概念创造 AI 能推理但不会”发明”新概念（如群、流形、范畴） ❌ 无迹象
4. 证明策略的广度 每个证明只需要几十步，但搜索空间指数级膨胀 ⚠️ 搜索优化中
5. 计算成本 一个 IMO 题的证明可能需要 GPU 数小时到数天 ⚠️ 硬件在进步
6. 反馈信号稀疏 真定理可以验证，但”有趣的方向”这种信号无法形式化 ❌ 根本性困难
7. 跨领域迁移 几何题的训练不能帮助数论 ⚠️ 多任务学习中

6.2 核心困难：证明与验证的非对称性

Gödel 的不完备性定理告诉我们：数学真理永远超越形式系统。这给 AI 数学推理带来了一个根本性的限制：

  • ✅ 验证一个证明是容易的（只要一个形式化内核检查每一步）
  • ❌ 寻找一个证明是困难的（搜索空间是无限的）

AI 系统（如 AlphaProof）本质上是在做”大规模搜索 + 学习启发式”——它不会”理解”数学，它学会的是”什么形状的搜索树更容易成功”。

但这并不意味着 AI 没有用——人类数学家的工作流中，90% 的时间也消耗在”搜索”（失败的尝试）上。AI 可以在搜索阶段帮人类排除 90% 的无效路径。

七、对数学家的实际影响：工作流变革

我把 AI 对数学研究的影响分为三个层次：

7.1 当前已可用的（2025-2026）

能力 工具 实际效果
证明搜索辅助 AlphaProof / DeepSeek-Prover 提供已知定理的替代证明
引理验证 Lean + Copilot 自动检查复杂计算的正确性
反例搜索 符号计算 + SAT 求解器 快速验证猜想的反例存在性
文献回顾 LLM 辅助 从大量论文中提取关键技术

7.2 未来 3-5 年可预期的

  • “自动引理建议”：当你需要某个中间引理时，AI 自动从 mathlib 中推荐或自动推导
  • “证明草图扩写”：你写一个高层次证明草图，AI 将其展开为 Lean 可验证的完整证明
  • “猜想生成”：AI 基于已有定理的模式识别，提出可能的新猜想

7.3 我个人的预测

AI 不会取代数学家，但会用 AI 的数学家将会取代不用 AI 的数学家。

具体来说：

  • 定理发现：AI 会成为”助手”而非”创造者”
  • 证明验证：形式化验证将成为顶级期刊的投稿标准（类似今天的代码可复现性）
  • 数学教育：AI 导师将彻底改变数学教学（尤其是竞赛数学）
  • 数学家的核心能力：将从”计算和推导”转向”概念创新和形式化思维”

八、2025-2026 值得关注的趋势

8.1 技术与工程

  1. Lean 4 生态成熟：协程支持、更好的 IDE 集成、更快的编译速度
  2. 多模态证明搜索：组合几何（AlphaGeometry）+ 代数（AlphaProof）的统一框架
  3. 超长证明序列学习：从 50-step IMO 题到 1000-step 研究级定理

8.2 社区与文化

  1. 形式化数学的”Wikipedia 时刻”：更多数学家像编辑 Wikipedia 一样向 mathlib 贡献形式化定理
  2. AI 辅助的 arXiv 审核：自动检查论文中的逻辑错误
  3. 数学奥林匹克训练的新范式：选手用 AI 系统做陪练

8.3 关键论文（2024-2025）

论文 年份 核心贡献
AlphaGeometry (Nature, Trinh et al.) 2024.01 零示范几何推理
AlphaProof Technical Report (DeepMind) 2024.07 RL + Lean 的 IMO 银牌
DeepSeek-Prover v2 (DeepSeek AI) 2025.01 开源形式化证明 SOTA
Formalizing 100 Theorems (mathlib 社区) 2025 100 个经典定理的形式化里程碑

九、结论

2024-2025 年，AI 数学推理经历了从”实验室演示”到”竞赛银牌”的跨越。AlphaProof/AlphaGeometry 证明了神经-符号混合方法是有效的，DeepSeek-Prover 证明了开源路线可以快速追赶，Lean 社区的爆发证明了形式化数学正在从小众走向主流。

但我们也需要坦诚地面对：现在 AI 能做的是”解已知题”，而非”发现新数学”。这两个目标之间的距离，可能比从 IMO 0 分到银牌的距离还要大。

对于读者而言——无论你是数学家、工程师还是学生——现在开始接触 Lean 和 AI 辅助证明工具，可能是你今年最有价值的”时间投资”。

参考文献

  1. Trinh, T.H., Wu, Y., Le, Q.V., He, H., Luong, T. “Solving olympiad geometry without human demonstrations.” Nature, 625, 476–482 (2024). DOI: 10.1038/s41586-023-06747-5
  2. DeepMind. “AI achieves silver-medal standard solving International Mathematical Olympiad problems.” DeepMind Blog, July 2024.
  3. DeepSeek AI. “DeepSeek-Prover v2: Advancing Formal Theorem Proving.” arXiv, 2025.
  4. The mathlib Community. “Mathlib4: A Unified Formal Mathematics Library.” 2024-2025.
  5. Buzzard, K. “The Future of Mathematics?” Notices of the AMS, 2024.

本文基于公开的论文、技术报告和社区数据撰写。数据截至 2026 年 6 月。