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

一篇新论文首次大规模评估了使用大型语言模型（LLM）生成形式化证明来解决开放数学问题的能力。最先进的智能体以每个问题几百美元的成本，自主解决了353个开放Erdős问题中的9个，并验证了492个OEIS猜想中的44个，目前已部署在组合学、优化、图论、代数几何和量子光学等多个领域。研究表明AI辅助形式化证明搜索在数学研究中具有巨大潜力。