利用AI驱动的形式化证明搜索推进数学研究
一篇新论文首次大规模评估了使用大型语言模型（LLM）生成形式化证明来解决开放数学问题的能力。最先进的智能体以每个问题几百美元的成本，自主解决了353个开放Erdős问题中的9个，并验证了492个OEIS猜想中的44个，目前已部署在组合学、优化、图论、代数几何和量子光学等多个领域。研究表明AI辅助形式化证明搜索在数学研究中具有巨大潜力。
文章情报
要点
- 首次大规模评估LLM生成形式化证明解决开放数学问题的能力
- 最先进智能体以每问题数百美元的成本解决了9个Erdős问题
- 智能体还验证了44个OEIS猜想，并应用于多个数学领域
- 研究表明AI辅助形式化证明搜索在数学研究中的潜力
为什么重要
这条新闻值得关注，因为首次大规模评估LLM生成形式化证明解决开放数学问题的能力。
技术影响
可能影响模型选型、推理成本、产品能力和评测基准。
大型语言模型（LLM）在数学推理方面日益出色，但其不可靠性限制了其在数学研究中的实用性。一种缓解方法是利用LLM生成形式化证明，例如在Lean语言中。近期一篇题为《利用AI驱动的形式化证明搜索推进数学研究》的论文首次大规模评估了这种方法解决开放问题的能力。
该研究团队设计了一种智能体，它交替使用LLM生成证明和基于Lean的验证。最先进的智能体在353个开放Erdős问题中自主解决了9个，每个问题的成本仅为几百美元。此外，该智能体还成功证明了492个OEIS猜想中的44个。目前，这一方法已部署在组合学、优化、图论、代数几何和量子光学等研究领域。
论文还比较了不同智能体设计的效果。一个基本版本仅通过交替生成和验证也能解决部分Erdős问题，但在最困难的问题上成本更高。这些发现展示了AI辅助形式化证明搜索的强大能力，并揭示了实现这一能力的关键智能体设计要素。
该研究为数学研究开辟了新途径，使AI能够协助数学家探索开放问题，并有望在未来加速数学发现的进程。论文由George Tsoukalas等20位作者共同完成，于2026年5月21日提交至arXiv，主题为人工智能（cs.AI）。研究不仅证明了AI在数学证明中的可行性，还强调了成本效益和设计选择的重要性。随着LLM技术的进步和推理成本的降低，AI辅助证明搜索有望成为数学研究的常规工具，帮助解决更多长期困扰数学家的难题。