Advancing Mathematics Research with AI-Driven Formal Proof Search

📄 arXiv: 2605.22763v1 📥 PDF

作者: George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, Francisco J. R. Ruiz, Arun Suggala, Adam Zsolt Wagner, Eric Wieser, Lei Yu, Aja Huang, Miklós Z. Horváth, Andrew Ferrauiolo, Henryk Michalewski, Codrut Grosu, Thomas Hubert, Matej Balog, Pushmeet Kohli, Swarat Chaudhuri

分类: cs.AI

发布日期: 2026-05-21

备注: The first three authors and the last author have equal contributions. The first three authors are in random order

💡 一句话要点

利用AI驱动的形式化证明搜索推进数学研究

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式化证明 大型语言模型 数学推理 AI辅助 Lean 开放问题 定理证明

📋 核心要点

  1. 现有LLM在数学推理中表现出色，但其结果的不可靠性阻碍了其在严肃数学研究中的应用。
  2. 该研究利用LLM生成形式化证明，并使用Lean等工具进行验证，以提高数学推理的可靠性。
  3. 实验结果表明，该方法成功解决了部分开放的Erdős问题和OEIS猜想，并在多个数学领域展现了应用潜力。

📝 摘要（中文）

大型语言模型(LLMs)在数学推理方面表现越来越出色，但其不可靠性限制了它们在数学研究中的应用。一种缓解方法是使用LLMs生成诸如Lean等语言的形式化证明。我们首次大规模评估了这种方法解决开放问题的能力。我们最强大的agent以每个问题几百美元的成本自主解决了353个Erdős开放问题中的9个，证明了492个OEIS猜想中的44个，并正在被部署到组合数学、优化、图论、代数几何和量子光学研究中。一个基于LLM生成和Lean验证交替进行的基础agent复制了Erdős的成功，但在最困难的问题上成本更高。这些发现证明了AI辅助形式化证明搜索的力量，并阐明了实现它的agent设计。

🔬 方法详解

问题定义：论文旨在解决LLM在数学推理中可靠性不足的问题，现有方法难以保证数学证明的正确性，阻碍了LLM在数学研究中的应用。形式化证明可以提供严格的数学保证，但人工构建形式化证明成本高昂。

核心思路：论文的核心思路是结合LLM的生成能力和形式化验证工具的可靠性，利用LLM生成候选证明，然后使用形式化验证工具（如Lean）验证其正确性。通过这种方式，可以利用LLM的创造力，同时保证证明的严谨性。

技术框架：整体框架包含两个主要模块：LLM证明生成器和Lean验证器。LLM证明生成器负责根据给定的数学问题生成形式化证明的候选方案。Lean验证器则负责对LLM生成的证明进行形式化验证，判断其是否正确。如果验证失败，则反馈给LLM，LLM根据反馈进行调整，重新生成证明。这个过程迭代进行，直到找到一个被Lean验证通过的证明。

关键创新：最重要的创新在于将LLM的生成能力与形式化验证工具相结合，形成一个闭环的AI辅助证明系统。这种方法既利用了LLM的创造性，又保证了证明的严谨性。此外，论文还探索了不同的agent设计，例如基础agent和更强大的agent，并比较了它们在解决不同难度问题上的表现。

关键设计：论文中使用了多种LLM，并针对不同的数学问题进行了微调。在Lean验证方面，使用了标准的Lean库和工具。关键的设计在于如何有效地将LLM的输出转换为Lean可以理解的形式，以及如何设计反馈机制，使LLM能够根据Lean的验证结果进行改进。此外，还探索了不同的搜索策略，例如宽度优先搜索和深度优先搜索，以提高证明搜索的效率。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，该研究提出的方法成功解决了353个Erdős开放问题中的9个，证明了492个OEIS猜想中的44个。更强大的agent在解决复杂问题上表现更优，但成本也更高。基础agent在简单问题上表现良好，且成本较低。这些结果证明了AI辅助形式化证明搜索的有效性。

🎯 应用场景

该研究成果可应用于数学研究的多个领域，例如组合数学、优化、图论、代数几何和量子光学等。通过AI辅助形式化证明，可以加速数学研究的进程，发现新的定理和结论。此外，该方法还可以用于教育领域，帮助学生更好地理解和掌握数学知识。

📄 摘要（原文）

Large language models (LLMs) increasingly excel at mathematical reasoning, but their unreliability limits their utility in mathematics research. A mitigation is using LLMs to generate formal proofs in languages like Lean. We perform the first large-scale evaluation of this method's ability to solve open problems. Our most capable agent autonomously resolved 9 of 353 open Erdős problems at the per-problem cost of a few hundred dollars, proved 44/492 OEIS conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research. A basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes but proved costlier on the hardest problems. These findings demonstrate the power of AI-aided formal proof search and shed light on the agent designs that enable it.