据arXiv网站2026年5月21日消息，DeepMind最新研发的AI智能体AlphaProof Nexus，首次在研究级数学问题上实现大规模突破。该工具成功解决了9个长期未解的Erdős开放问题，其中最早一题已困扰学界56年。该工具还证明了44个OEIS数学猜想，并解决了悬置15年的纯O-序列对数凹性问题。该成果表明，形式化证明搜索已具备在较大规模问题集上系统运行的可行性，且求解成本显著降低，单题成本最低仅为7.5美元。

该智能体的核心突破在于将大语言模型与Lean形式化验证系统深度结合，克服了传统大模型数学推理易产生“幻觉”且难以验证的痛点。智能体以Gemini 3.1 Pro为推理引擎生成证明草图，由Lean编译器检查验证并反馈修正，形成闭环迭代。为提升复杂问题求解效率，智能体还引入强化学习模型处理局部子目标，并采用进化式搜索机制，通过共享草图库与评分模块，优先筛选并沿着更有潜力的证明路径进行搜索。

目前，该智能体已在组合数学、代数几何及量子光学等真实数学研究中取得具体成果。然而，其能力仍局限于Lean数学库等相对成熟的领域，多数开放问题仍超出其求解范围，且系统存在继承底层大模型偏差、搜索波动较高等问题。此外，单题低成本并不包含前期大规模筛题的算力消耗。

信息来源：

https://arxiv.org/abs/2605.22763v1

https://mp.weixin.qq.com/s/jM_lkCGRbhrwz4_ydMCCVA