数学研究者终于有了能真正解决开放问题的 AI 工具——成本可控且覆盖多个数学分支，做组合数学或图论的人可以直接用这个智能体尝试自己的猜想。
研究人员首次大规模评估了用大语言模型生成形式化证明（Lean 语言）解决开放数学问题的能力。其最强大的智能体以每个问题几百美元的成本，自主解决了 353 个开放 Erdős 问题中的 9 个，并证明了 492 个 OEIS 猜想中的 44 个。该智能体已被部署在组合数学、优化、图论、代数几何和量子光学研究中。一个更基础的智能体（交替 LLM 生成与 Lean 验证）也复现了 Erdős 问题的成功，但在最难问题上成本更高。这些结果展示了 AI 辅助形式化证明搜索的潜力，并揭示了实现这一能力的智能体设计。
Advancing Mathematics Research with AI-Driven Formal Proof Search
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.