DeepMind 研究：AI 智能体自主解决 9 个 Erdős 开放问题

Google DeepMind 团队近日在 arXiv 上发表论文《Advancing Mathematics Research with AI-Driven Formal Proof Search》，首次大规模评估了基于大语言模型（LLM）的形式化证明搜索智能体在开放式数学问题上的实际能力。该工作由 Swarat Chaudhuri、Pushmeet Kohli 等 DeepMind 研究人员主导，论文编号 arXiv:2605.22763。

核心成果

研究团队构建了一套让 LLM 在 Lean 等形式化证明语言中自动生成证明的智能体系统，并在三类真实数学问题上进行了大规模实证：

• 在 353 个 Erdős 开放问题中，最强智能体自主解决了 9 个；
• 在 492 个 OEIS 猜想中，该智能体成功证明 44 个；
• 每个问题的平均成本仅为「数百美元」级别；
• 该系统正在被组合数学、优化、图论、代数几何、量子光学等领域的研究者实际部署使用。

方法与智能体设计

论文对比了两种智能体设计思路：

• 强智能体：具备更强的自主推理与策略选择能力，能够独立处理高难度的开放问题；
• 基础智能体：采用「LLM 生成—Lean 验证」交替循环的简单模式。

结果显示，基础智能体在 Erdős 问题集上能够复现强智能体的成绩，但在最难的问题上代价显著更高。这表明，简单的生成-验证循环已具有相当能力，但要高效攻克最困难的开放问题，仍需要更复杂的智能体设计。

研究意义

论文标题中的关键词是「first large-scale evaluation」。此前虽有 LLM 证明形式化定理的工作（如 LeanDojo、Lean-GitHub 等），但学界一直缺乏这类方法在「公开且未解问题」上的系统性验证。该研究的价值正是在于：

• 提供了端到端、可量化的实证证据，证明 AI 辅助形式化证明已具备参与一线数学研究的实用潜力；
• 揭示了不同智能体架构在成本与能力上的权衡，为后续研究指明了方向；
• 单题「数百美元」的成本数据，使该方法具备可大规模推广的经济性。

局限与展望

论文同时也指出，LLM 本身在数学推理上仍存在不可靠性，不能直接用于代替人类数学家。当前的工作模式是 AI 生成候选证明，由形式化系统与研究者共同把关。从研究范式看，这更像是一种「人机协作」而非「AI 替代」——但 9 个 Erdős 问题的突破，已经显示出该范式正在快速走向成熟。