谷歌DeepMind推出AlphaProof Nexus：自主解决9个Erdős开放问题

5月26日，谷歌DeepMind最新推出AlphaProof Nexus，该系统结合大语言模型生成证明与Lean形式化验证，在353个开放的Erdős问题中自主解决了9个，并解开了2个悬而未决56年的数学难题。Lean是一种形式化证明语言和证明助手系统，研究者可将数学命题、定义和证明步骤写成严格可检查的代码，由编译器逐步判断合法性。Erdős问题是由20世纪最高产的匈牙利数学家保罗·埃尔德什提出的一系列数学猜想和问题，涵盖组合数学、数论、图论和几何等领域。

根据谷歌论文，AlphaProof Nexus在353个开放的Erdős问题中解决了9个，其中2个已悬而未决56年。该系统还在OEIS的492个开放猜想中证明了44个，解决了1个存在15年的Hilbert函数问题，并改进了凸优化中的已知界限。每个问题的推理成本仅需数百美元。

架构方面，AlphaProof Nexus由4个复杂度递增的AI智能体组成：Agent A仅依赖Gemini 3.1 Pro与Lean编译器循环交互；Agent B接入AlphaProof补全缺失证明片段；Agent C加入类似AlphaEvolve的进化机制，让多个证明草稿共享、评分、排序；功能最完整的Agent D整合了上述能力。研究团队发现，最简单的Agent A也能证明这9个已解问题，只是在最难题目上花费更高。这反映出两个变化：底层模型能力持续提升，以及编译器反馈对LLM推理的“锚定”作用越来越强。