谷歌 DeepMind 近期推出了一项名为 AlphaProof Nexus 的人工智能框架，该系统创造性地将大型语言模型（LLM）生成数学证明的能力与 Lean 形式化验证工具相结合，在数学领域取得了显著突破。
在由著名匈牙利数学家保罗·埃尔德什提出的 353 个开放性数学问题中，AlphaProof Nexus 成功自主解决了 9 个，其中两项问题已困扰数学界长达 56 年。此外，该系统还在整数序列在线百科全书（OEIS）的 492 个开放猜想中验证了 44 个，并攻克了一个存在 15 年的希尔伯特函数问题，同时还在凸优化领域改进了已知的边界条件。值得一提的是，处理每个问题的推理成本仅为数百美元。
Lean 是一种形式化证明语言和辅助系统，允许研究人员以严格可检查的代码形式表述数学命题、定义和证明步骤，并通过编译器逐一验证其合法性。Erdős 问题则涵盖了组合数学、数论、图论和几何等多个数学分支领域，是 20 世纪最活跃的数学家之一埃尔德什提出的一系列具有挑战性的猜想和问题。
AlphaProof Nexus 的架构由四个复杂程度递增的 AI 智能体构成。最简单的 Agent A 仅依赖 Gemini 3.1 Pro 模型与 Lean 编译器进行循环交互；Agent B 在此基础上引入 AlphaProof 模块以补全缺失的证明片段；Agent C 则集成了一种类似 AlphaEvolve 的进化机制，能够对多个证明草稿进行共享、评分和排序；而功能最为全面的 Agent D 则整合了上述所有能力。
研究团队最初预期使用最强大的 Agent D 来攻克 Erdős 问题，但意外发现，即便是最基础的 Agent A，也能够成功证明这 9 个已解决的问题，尽管它在面对最困难题目时会花费更多资源。这一发现凸显了两个关键趋势：底层模型能力的持续增强，以及编译器反馈在大型语言模型推理过程中发挥着越来越重要的“锚定”作用。