大家好，我是HxShine，前段时间，Nature封面被AI Scientist刷屏，但在Math领域，AI究竟达到了什么样的水平了呢？

今天结合 Google DeepMind 的一篇文章，我们一起来看看当前AI能解决多少前沿数学问题， 文章为：Advancing Mathematics Research with AI-Driven Formal Proof Search（利用AI驱动的形式化证明搜索推进数学研究）。结论如下：

在未经人类干预的情况下，在他们搭建了一个AlphaProof Nexus 框架下，**自主解决了包括56年未解之谜在内的9个 Erdős 开放问题，以及 44 个 OEIS 未解猜想。**而且发现该系统不仅在竞赛数学中大放异彩，也能在组合数学、图论、优化理论和代数几何等真实数学研究前沿做出实质性贡献。

未来，数学家在科研中应该扮演什么样的角色呢？

一、概述

• Title: Advancing Mathematics Research with AI-Driven Formal Proof Search
• URL: https://arxiv.org/abs/2605.22763v1?ref=airadar.one
• Authors: George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, 等 (Google DeepMind, Aarhus University, Google)
• Code: https://www.github.com/google-deepmind/alphaproof-nexus-results

1 Motivation

这篇文章主要尝试解决这两个问题：

• 如何降低LLM在数学研究中的幻觉？ 一些细微的幻觉，人类审核起来太耗时耗力。
• LLM在解决一些未解的，前沿级别的数学问题究竟表现如何？ 对于一些开放的，前沿的问题，LLM究竟到哪一步了，能解决多少？

2 Methods

采用了一个叫做 AlphaProof Nexus 框架。基座模型采用了最新的Gemini 3.1 Pro和Gemini 3.1 flash构建Agent Loop，并利用 Lean 编译器提供绝对严谨的编译反馈。

特点：

• Elo评分：解决形式化证明二元结果的连续评分问题，可以用于根据推理路径筛选高质量的评估结果。
• 支持human in the loop输入知识：最上面支持数学家human in the loop输入知识。
• 结合gemini 3.1 pro和gemini 3.1 flash进行推理，balance成本和效率。
• 结合多种工具：AlphaProof以及Lean相关工具。

**构建4种变体Agent：**为了探索哪种Agent Loop更有效，其构建了4类智能体，具体如下：

智能体	核心组件	关键工作流程	工具 / 模型
Agent A (基础)	独立并行的 Prover 子智能体（无共享状态）	每个子智能体运行多轮 “Ralph loop”：LLM 通过思维链推理，使用 search_replace 修改 Lean 草图 → 调用 Lean 编译器验证 → 利用报错信息引导下一轮修改；若死胡同则总结经验回退。	LLM (Gemini 3.1 Pro) + Lean 编译器
Agent B (基础 + AlphaProof)	Agent A 架构 + AlphaProof 调用权限	LLM 将证明分解为子目标，交给 AlphaProof 求解 → AlphaProof 返回证明/反证/失败信息 → 结果直接反馈进 LLM 的 Prompt，继续迭代。	LLM (Gemini 3.1 Pro) + Lean + AlphaProof
Agent C (基础 + 进化算法)	种群数据库 + Prover 智能体 + Rater 智能体	① Prover 从数据库采样草图进行修改，成功草图放回数据库；② Rater（低成本LLM）对未完成草图两两对决，计算 Elo 评分；③ 基于 P-UCB 策略按 Elo 评分采样高潜力草图继续探索。	Prover: LLM (Gemini 3.1 Pro) Rater: LLM (Gemini 3.0 Flash)
Agent D (全功能)	Agent B + Agent C 能力的结合	既使用进化算法协调多智能体全局搜索（种群 + Elo + P-UCB），又允许 LLM 在需要时调用 AlphaProof 攻克具体子目标。文章主要发现（解决开放问题）均由该智能体测得。	LLM (Gemini 3.1 Pro / 3.0 Flash) + Lean + AlphaProof + 进化框架

3 Experiments

在 353 个 Erdős 问题和 492 个 OEIS 猜想上进行了大规模评估，发现基础智能体足以解决所有测试的开放问题，但全功能智能体在最具挑战性的题目上能以更低的资金成本获得更高效率。

详细实验设置如下：

类别	详细描述
实验数据	① 来自 Formal Conjectures 仓库的 353 个 Erdős 开放问题（已形式化）；② 492 个 OEIS 未解猜想（自动形式化）；③ 代数几何、凸优化、图论、量子光学等前沿研究级问题。
Baseline 方案	① 树搜索模式下的独立 AlphaProof；② 使用 Gemini 3.0 Flash 的基础智能体；③ Agent A/B/C 互为基线，最终对比 Agent D（全功能）。
实验设置	① 核心推理模型：Gemini 3.1 Pro，评分模型：Gemini 3.0 Flash；② 成本以 USD 统一核算（API token 定价）；③ 基础智能体：100 次独立尝试，进化智能体：10 次尝试，绘制解决率‑成本的 Pareto 前沿；④ 单个问题最大迭代：3000 步。
实验内容	① 主实验：解决 9/353 个 Erdős 问题（含 56 年未解难题），证明 44/492 个 OEIS 猜想；② 跨领域部署：在图论（重构猜想变体）、凸优化（新学习率发现）、代数几何（15 年悬案）、量子光学（GHZ 态构造）取得新成果；③ 消融分析：Agent A 可解决全部 9 个问题，但对最难题目（如 #125）Agent D 的成本效益显著更优。

4 Conclusion

• AI目前已经能自主解决研究级数学开放问题： 证明了 LLM 不仅仅能做做题，而且已经有能力自主攻克存在了几十年的开放性数学研究问题（如 Erdős 猜想）。

这里展示的是一个例子：Erdos问题 #125）AI Agent结合Lean环境 + AlphaProof工具解决高难度问题。

• 简单 Agentic Loop 就能解决大部分问题，但是难题还是得上自进化版本并结合AlphaProof工具： 随着基座模型能力的提升，简单的“生成-编译反馈”循环（基础智能体）已经非常强大；但在最困难的数学推导上，融入 AlphaProof 和基于 Elo 的进化搜索反而成本更低。

• 未来数学家+AI Scientist助手的人机协同模式将成为新范式： 即使 AI 未能完整证明问题，其生成的形式化草图也能帮助人类数学家聚焦于未解决的子目标，并有效发现人类原始论文或猜想中的“形式化错误（Misformalizations）”。

---

二、详细内容

1 解决的问题汇总：都是一些可能存在了几十年的待解决的问题，太强了!

• **说明：**目前智能体成功解决的 9 个 Erdős 开放问题。表格列出了：问题 ID、猜想的年代与简述（如1970年提出的强除法约束问题、1996年的下密度问题等）以及 AI 采用的证明策略（如基于中国剩余定理的分块构造、丢番图逼近等）。

2 不同Agent的成本-成功率折线图

• 说明: 横坐标为平均推理成本（美元），纵坐标为求解率。对比了 Agent A, B, C, D 四种架构。在简单问题上架构差异不大，但在困难问题（如 erdos_125）上，全功能系统(D)性能遥遥领先的现象。
• 要点总结：
  1. “简单即美”是常态：对于大多数开放问题，一个设计简单、简单的Agent（Agent A或B）就足够优秀，成本效益最高。
  2. “复杂Agent架构攻坚难题成本更低”：进化框架+AlphaProof的设计（Agent D）并非普遍适用（简单题都用不上Agent D），但在更难的一些题目的时候，成本更低。所以对于一些难的题目，直接上全能型的AgentD就行。
  3. 工具至关重要（这里把AlphaProof当作一个工具）：对比Agent A和B，可以看到，在不改变核心搜索策略的前提下，仅仅赋予LLM调用一个强大的专用证明器的能力，就能在多个问题上改善成本效益。
  4. 一句话总结：“如果你面对的是常规难题，直接用基础Agent；如果是在屡试不得其解的超级难题上，直接用Agent D模式。

---

三、总结

结论1: AI 已经能解决高难度的前沿数学问题。 就算基础的Agent都已经具备了自主攻克封尘数十年、具有极高学术价值的数学开放难题（如保罗·埃尔德什的猜想）的能力，标志着 AI 数学向真实科研级别跨越。

结论2: “强大的工具 + Agent Loop + 自进化能解决一些高难度问题，并且成本更低。 强大的基座大模型负责发散思维、分解任务；形式化编译器Lean提供高质量反馈，即使不加复杂的RL算法，当前LLM也具备强大的自我修正和推理能力，并能解决高难度的问题。

👇关注公众号NLP PaperWeekly，及时获取最新前沿资讯👇