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