【AlphaProof Nexus: 批量破解数学难题】

5月21日，DeepMind发表论文，介绍了大语言模型驱动的定理证明系统AlphaProof Nexus。它让大语言模型在 Lean 形式化证明系统中搜索证明，每一步都由机器检查。实验中，最强智能体在353个开放 Erdős 问题中自主解决了9个，其中包括两个56年悬而未决的问题；它还证明了492个 OEIS 开放猜想中的44个。这个系统还很省钱，每道题的证明成本只有几百美元。AI批量破解数学难题的日子到来了。

参考文献：Tsoukalas G, Kovsharov A, Shirobokov S, et al. Advancing Mathematics Research with AI-Driven Formal Proof Search[J]. arXiv preprint arXiv:2605.22763, 2026.
#人工智能##ai创造营#