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

大型语言模型（LLM）在数学推理方面表现日益卓越，但其不可靠性限制了在数学研究中的效用。一种缓解策略是利用 LLM 生成如 Lean 等形式化语言的证明。本文首次对该方法解决开放性问题的能力进行了大规模评估。结果显示，最先进的智能体以每题数百美元的成本，自主解决了 353 个埃尔德什开放问题中的 9 个，并证明了 492 个 OEIS 猜想中的 44 个，目前已部署于组合学、优化等多个领域。研究证实了 AI 辅助形式化证明搜索的强大能力，并揭示了实现该能力的关键智能体设计。