数学中的人工智能 — 证明、形式化与猜想
数学是机器推理最干净的压力测试：一个命题非真即假，而形式化证明是可机械检验的。 这一特性使数学成为 ai-for-science 的旗舰子学科——与湿实验室生物学不同，数学的 验证器免费、精确且不可腐化。2024–2026 年的前沿可分为两种正在融合的研究文化：写出 人类风格自然语言证明的非形式化大语言模型（LLM）推理，以及在 Lean、Isabelle 或 Coq 中产出机器可验证证明的形式化系统。两种文化中占主导的制胜范式都是神经符号： LLM 提出方案，符号引擎验证，搜索循环弥合二者间的鸿沟。
本模块仅从 AI/ML 角度展开——聚焦学习系统、其训练循环，以及其基准分数意味着什么、 不意味着什么。
1. 定理证明
形式化证明（机器检验）
AlphaProof（见 alphaproof）是 Google DeepMind 的旗舰形式化证明器。它将一个 预训练语言模型与 AlphaZero 强化学习（RL）算法耦合，在 Lean 证明环境内部运行， 从而每个候选证明都被自动验证 [1]。其训练依赖将约 8000 万条自然语言问题陈述自动形式化 为 Lean，以引导 RL 自博弈循环 [1]。在 2024 年国际数学奥林匹克（IMO）上， AlphaProof——与 AlphaGeometry 2 联手——解出 6 题中的 4 题，得 42 分中的 28 分， 恰为银牌门槛、仅差金牌一分；这是首次有 AI 达到 IMO 奖牌层级 [1]。完整方法于 2025 年 发表于 Nature [2]。AlphaProof 负责代数与数论题，几何题交由 AlphaGeometry 2。
AlphaGeometry / AlphaGeometry2 是专精的神经符号几何系统：语言模型提出辅助构造， 符号演绎引擎推导出所有结论。AlphaGeometry2 将 2000–2024 年 IMO 几何题的求解率提升至 84%（第一代为 54%），在该题集上超越了人类金牌选手的平均水平 [3]。在 IMO 2025 上， 它直接从自然语言出发，约 20 秒内解出几何题（P2）[3]。
DeepSeek-Prover 是领先的开源权重形式化证明器。DeepSeek-Prover-V2（671B， 2025 年 4 月）针对 Lean 4 验证器训练一个 RL 证明生成器，先用 DeepSeek-V3 将定理分解为 子目标，再进行递归证明搜索 [4]。它在 miniF2F-test 基准上达到 88.9% 通过率 （V1.5 约为 63.5%），并在 PutnamBench 658 题中解出 49 题，权重公开发布 [4]。 Kimina-Prover 是并行的开源努力，将 RL 应用于大型形式化推理模型，并开源了 用于自然语言→Lean 4 翻译的 Kimina-Autoformalizer [5]。
非形式化证明（自然语言，LLM）
到 2025 年，前沿 LLM 开始在非形式化奥赛推理上比肩顶尖人类。Gemini Deep Think （高级版）在 IMO 2025 上正式获得 35/42——解出 6 题中的 5 题，是首个获得官方认证 金牌分数的 AI，在 4.5 小时考试窗口内全程以自然语言端到端作答 [6]。OpenAI 另行报告 一款实验模型也取得 35/42，但未经 IMO 官方认证 [6]。这些是由人类评分的非形式化证明， 并非机器检验——这正是区别于 AlphaProof 形式化输出的核心警示。
2. 自动形式化
自动形式化是把自然语言数学翻译成形式语言（通常是 Lean 4），以便机器验证。它是连接 非形式化与形式化两种文化的承重桥梁，也是当前最薄弱的一环。AlphaProof 的 8000 万条 陈述训练流水线本身就是一个自动形式化引擎 [1]。
ProofNet（本科水平的自动形式化+证明）及其修订版 ProofNet#、以及 miniF2F 是标准 测试平台。诚实的最新状况是：即便前沿模型也难以产出类型正确的 Lean 4，但采样多个候选 并过滤掉类型错误的输出可带来巨大提升，且准确率随形式化尝试预算增大而持续上升 [5]。 专用的 7B 自动形式化器（如 Kimina-Autoformalizer）直接针对该任务 [5]。尚未解决的难题是 忠实性：一条命题可能在 Lean 中编译通过，却并不表达英文原意——由改写引发的误译仍是 活跃的失败模式。
3. LLM 在数学基准上的推理
如今有一整套递进的基准来追踪前沿模型的数学能力：
- MATH / AIME —— 答案为短数字的竞赛题。前沿推理模型已基本饱和 MATH，并在 AIME 上 取得高分；由于这些题目广为公开，数据污染（模型在预训练中已见过题目）是严重的混淆 因素，故高分须谨慎解读。
- Putnam / PutnamBench —— 本科竞赛；PutnamBench 提供形式化（Lean）目标，因而抗污染。 DeepSeek-Prover-V2 在 658 题中解出 49 题 [4]。
- FrontierMath（Epoch AI）—— 数百道原创、由专家精心编制的题目，覆盖从数论到代数几何， 许多题需专家耗时数小时乃至数天；数据集（4 个层级共 338 题）未公开以抗污染 [7]。它是 最难的标准数学基准；以往即便强模型也仅得两位数低分，不过截至 2026 年领先者已大幅攀升。
AI 数学奥林匹克（AIMO）奖（由 XTX Markets 资助）举办 Kaggle 竞赛，目标是开源出 IMO 金牌水平的模型。首届进步奖（2024）由 Numina 团队（NuminaMath）夺得，奖金 131,072 美元；颁奖在 IMO 2024 上由陶哲轩主持 [8]。第二届进步奖由英伟达的 NemoSkills 团队 夺得，第三届奖项随后启动 [8]。
"解出"意味着什么——诚实说明。 "解出"一词背后藏着三种截然不同的主张： （a）机器检验的形式化证明（AlphaProof、DeepSeek-Prover）——保证最强； （b）人类评分的自然语言证明（Gemini/OpenAI 在 IMO 2025）——由人而非机器验证； （c）数值基准（MATH、AIME）上的正确最终答案——它对推理是否有效只字未说。 污染对（c）威胁最大，形式化基准抗污染最好，而"给出正确数字"与"给出严密证明"之间的鸿沟 正是本领域的核心张力。
4. 猜想生成与数学发现
除了证明给定命题，AI 如今还被用来发现新数学。
FunSearch（DeepMind，Nature 2023）将一个 LLM 与自动评估器配对，置于对程序 （而非证明）的进化搜索之中。它为极值组合学中的**帽集问题（cap set）*产出了真正全新的 构造——这是 20 年来对其渐近下界的最大改进——并为在线装箱问题给出了新启发式 [9]。 关键技巧在于：LLM 提出的是程序代码*，外部评分器提供基准真值，从而规避 LLM 的幻觉。
DeepMind × 牛津/悉尼（Nature 2021）用 ML 引导数学家直觉，催生了纽结理论中的 一条新定理（代数不变量与几何不变量之间的联系），以及表示论中 Kazhdan–Lusztig 猜想 的进展 [10]。这里 AI 浮现出候选关系，由人类完成证明。
**拉马努金机器（Ramanujan Machine，Nature 2021）**通过数值匹配，为基本常数（π、e、 卡塔兰常数、ζ 函数值）自动生成连分数公式猜想——产出不带证明的猜想，部分后由他人证明 [11]。 它先于 LLM 时代，却是"以搜索促发现"范式的典范。
5. 神经符号范式
几乎所有旗舰成果背后的统一架构：
LLM 提出者 → 候选（证明步骤 / 构造 / 程序）
│
▼
形式化验证器 （Lean / 符号引擎 / 评估器） → 精确奖励
│
▼
搜索 / RL 循环 （树搜索、进化、AlphaZero） → 改进的提出者
验证器正是数学的特殊之处：它把不可靠的生成模型转化为可靠系统，因为未通过检验的东西 绝不会离开循环。这与 aifs-ml-self 中描述的自我改进 ML 系统所用的"提出者-验证器-搜索" 骨架同源，只是被专门化到了一个拥有免费神谕的领域。
系统对照表
| 系统 | 方法 | 结果 | 年份 |
|---|---|---|---|
| AlphaProof + AlphaGeometry 2 | Lean 内 LLM + AlphaZero RL；符号几何 | IMO 2024 银牌，28/42，解出 4/6 [1][2] | 2024 |
| AlphaGeometry2 | LLM 提出者 + 符号演绎 | 2000–2024 IMO 几何题 84%；IMO 2025 约 20 秒解 P2 [3] | 2025 |
| DeepSeek-Prover-V2 (671B) | RL + 子目标分解，Lean 4 验证器 | miniF2F-test 88.9%；PutnamBench 49/658 [4] | 2025 |
| Kimina-Prover / Autoformalizer | RL 形式化推理 + NL→Lean 翻译 | 开源权重证明器 + 自动形式化器 [5] | 2025 |
| Gemini Deep Think（高级版） | 非形式化 LLM，并行推理 | IMO 2025 金牌，35/42，5/6（人类评分）[6] | 2025 |
| FunSearch | LLM + 进化程序搜索 | 帽集新下界；装箱启发式 [9] | 2023 |
| 拉马努金机器 | 数值猜想搜索 | 常数的新连分数猜想 [11] | 2021 |
| DeepMind × 牛津 | ML 引导直觉 | 纽结理论定理；KL 猜想进展 [10] | 2021 |
基准对照表
| 基准 | 测试内容 | 污染风险 | 备注 |
|---|---|---|---|
| MATH / AIME | 竞赛，数值答案 | 高（已公开） | 已基本被前沿推理模型饱和 |
| Putnam / PutnamBench | 本科竞赛；Lean 目标 | 低（形式化） | DeepSeek-Prover-V2：49/658 [4] |
| miniF2F | 奥赛/AIME 级形式化证明（Lean） | 低（形式化） | DeepSeek-Prover-V2：88.9% [4] |
| ProofNet / ProofNet# | 自动形式化 + 证明 | 低 | 难点在忠实形式化 [5] |
| FrontierMath（Epoch） | 原创研究级题目 | 极低（未公开）[7] | 最难的标准基准 |
开放问题
- 验证成本。 形式化证明保证可靠性但代价高昂：据报道 AlphaProof 每道 IMO 题需大量算力， 而 DeepSeek-Prover 的最高分数依赖每条定理数千次采样 [4]。扩展证明搜索仍是瓶颈。
- 新颖 vs. 记忆。 在已公开基准（MATH、AIME）上，确实很难区分推理与背诵。抗污染的未公开 题集（如 FrontierMath [7]）与形式化目标（如 PutnamBench）是本领域的应对之策，但"这是否 是新数学？"的严格判定尚未解决。
- 自动形式化鸿沟。 把自然语言数学翻译成忠实、类型正确的 Lean，是连接非形式化 LLM 推理与 形式化验证的咽喉。采样加过滤有所帮助，但改写下的语义保持仍未解决 [5]。
- 非形式化却未检验的证明。 IMO 金牌级自然语言证明（Gemini、OpenAI）是人类评分而非机器 验证 [6]——把完整证明（而非仅最终答案）的循环闭合到机器可检验的输出，是下一个前沿。
- 超越基准的发现。 FunSearch 与各类猜想机器表明 AI 能产出真正的新结果 [9][11]，但仅限于 狭窄、可评分的领域；通用的开放式数学发现仍是愿景。
来源
- https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/ (2026-06-14)
- https://www.nature.com/articles/s41586-025-09833-y (2026-06-14)
- https://arxiv.org/abs/2502.03544 (2026-06-14)
- https://arxiv.org/abs/2504.21801 (2026-06-14)
- https://arxiv.org/abs/2504.11354 (2026-06-14)
- https://deepmind.google/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/ (2026-06-14)
- https://epoch.ai/frontiermath/the-benchmark (2026-06-14)
- https://aimoprize.com/updates/2024-07-20-progress-prize-results (2026-06-14)
- https://www.nature.com/articles/s41586-023-06924-6 (2026-06-14)
- https://www.nature.com/articles/d41586-021-03593-1 (2026-06-14)
- https://www.nature.com/articles/s41586-021-03229-4 (2026-06-14)