利用AI驅動的形式化證明搜索推進數學研究

一篇新論文首次大規模評估了使用大型語言模型（LLM）生成形式化證明來解決開放數學問題的能力。最先進的智能體以每個問題幾百美元的成本，自主解決了353個開放Erdős問題中的9個，並驗證了492個OEIS猜想中的44個，目前已部署在組合學、優化、圖論、代數幾何和量子光學等多個領域。研究表明AI輔助形式化證明搜索在數學研究中具有巨大潛力。