近日，谷歌DeepMind推出了一款名为AlphaProofNexus的人工智能工具，它结合了大型语言模型（LLM）和形式化验证系统Lean，以自主解决数学问题。AlphaProofNexus在353个开放的Erdős问题中成功解决了9个，其中包括两个悬而未决56年的问题。Erdős问题是由匈牙利数学家保罗·埃尔德什提出的一系列数学猜想和问题，覆盖了组合数学、数论、图论和几何等多个领域。

AlphaProofNexus还在OEIS（整数序列在线百科全书）的492个开放猜想中证明了44个，并解决了一个存在15年的Hilbert函数问题，同时改进了凸优化中的已知界限。每个问题的推理成本仅为数百美元。AlphaProofNexus由四个复杂度递增的AI智能体组成，从仅依赖Gemini3.1Pro与Lean编译器循环交互的AgentA，到整合了上述能力的AgentD。研究团队发现，即使是最简单的AgentA也能证明这9个已解问题，尽管在最难的题目上花费更高。

研究团队认为，这一成果反映出底层模型能力的持续提升以及编译器反馈对LLM推理的“锚定”作用越来越强。这项技术的发展不仅展示了AI在数学研究中的潜力，也预示着未来可能在更广泛的领域内应用AI进行形式化证明和问题解决。