收录解读
This paper evaluates LLM-driven formal proof search on open mathematical problems, using Lean-style formal verification as the reliability layer for generated proofs.
The reported system autonomously resolves several open Erdős problems and proves additional OEIS conjectures, showing that formal proof agents can move beyond benchmark exercises into active mathematical research workflows.
The important pattern is not just stronger math reasoning, but a workflow: generation, formal checking, search, cost control, and deployment into real combinatorics and related research contexts.
For this repository, it is a high-value AI-for-math entry because it demonstrates a reusable operating loop for reliable AI-assisted discovery where correctness can be machine-verified.
原始摘要与中文对照
中文对照翻译
大型语言模型（LLMs）在数学推理方面表现越来越出色，但其不可靠性限制了它们在数学研究中的效用。一种缓解方法是使用LLMs生成Lean等语言的正式证明。我们首次对这种方法解决开放问题的能力进行了大规模评估。我们最强大的智能体以每个问题几百美元的成本自主解决了353个开放的Erdős问题中的9个，证明了492个OEIS猜想中的44个，并且正在组合学、优化、图论、代数几何和量子光学研究中部署。一个将基于LLM的生成与基于Lean的验证交替进行的基本智能体复制了Erdős的成功，但在最困难的问题上成本更高。这些发现展示了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.