Google DeepMind 的 AlphaProof Nexus 以几百美元的成本解决数十年未解的数学问题
AlphaProof Nexus 花几百美元就解决了数学家 56 年没做出来的问题，虽然成功率只有 2.5%，但这条路证明形式化验证+强化学习是走得通的，做推理的该盯着看了。
Google DeepMind 的 AlphaProof Nexus 自主解决了 9 个开放的 Erdős 问题，其中包括两个困扰数学界 56 年的难题。其推理成本低至每个问题仅需几百美元。系统通过 Lean 编译器验证每个证明步骤，而非使用 OpenAI 的自然语言方法。当前的整体问题解决成功率为 2.5%。
Google DeepMind 的 AlphaProof Nexus 以区区几百美元成本攻克了数十年悬而未决的数学难题。
AlphaProof Nexus 将大语言模型驱动的证明生成与机器验证相结合，攻克了令数学家困惑数十年的数学研究问题。
Google DeepMind 的新框架 AlphaProof Nexus 已自主解决了它尝试的 353 个埃尔德什开放问题中的 9 个，其中包括两个长达 56 年无人解答的问题。
该系统还证明了来自整数序列在线百科全书（OEIS）的 492 个开放猜想中的 44 个，解决了代数几何中一个关于希尔伯特函数的 15 年悬而未决的问题，并改进了凸优化中的一个已知界限。根据研究论文，每个问题的推理成本仅为几百美元。
与 OpenAI 近期解决方案那种（可能）纯粹自然语言的方法不同，AlphaProof Nexus 中的底层语言模型——本例中是 Gemini 3.1 Pro——无需独自承担整个逻辑链条。
相反，它用 Lean 的形式化语言生成证明步骤，然后由编译器逐一检查。错误信息直接反馈到下一次尝试中。这样，大语言模型通过符号反馈得到了锚定——一个抵消语言模型在逻辑推理方面众所周知弱点的安全网。人类只在最后介入，检查结果。
四个智能体，一个令人惊讶的结论
该系统由四个复杂度递增的智能体变体组成。最简单的 Agent (A) 部署独立的子智能体，在循环中运行 Gemini 3.1 Pro：大语言模型生成证明步骤，Lean 编译器检查它们，错误信息反馈到下一次尝试中。
Agent (B) 增加了对 AlphaProof 的查询——Google 基于强化学习的奥数系统——它可以填补缺失的证明片段。Agent (C) 引入了进化组件。受 AlphaEvolve 启发，子智能体共享一个共同的证明草图种群。基于 Gemini 3.0 Flash 构建的评分智能体对这些草图的合理性和新颖性进行评分，然后使用 Elo 系统进行排序。完全装备的 Agent (D) 结合了所有这些能力。
Agent (D) 被用于埃尔德什问题。但事后分析发现了一个意外：最简单的 Agent (A)（仅使用大语言模型和编译器反馈）也能证明所有九个已解决的埃尔德什问题，尽管在最难的几个问题上成本更高。
研究人员将这种简单智能体的成功归因于两个因素：底层语言模型的快速改进，以及“编译器反馈在 grounding LLM 推理中的强大作用”。配置齐全的智能体在目前最困难的任务上仍具优势，但随着大语言模型的进步，这一领先优势可能会缩小。研究人员表示，这指向一个更大的趋势，他们将其描述为“随着大语言模型能力的增强，从专门的训练系统向简单智能体循环的持续转变”。
即便没有完整证明，系统依然有用
该系统的成功主要集中在组合数学、凸优化和数论等领域，在这些领域，Lean 的数学库 Mathlib 已相当成熟，且问题可以分解为可管理的子目标。大部分 Erdős 问题仍无法触及，“更不用说那些需要大量新理论的问题了”，研究人员写道。智能体也继承了底层语言模型的不可靠性。
尽管如此，他们看到了超越解题本身的价值。使用该系统的数学家报告称，即使是失败的证明尝试也加深了他们对问题的理解，或者如作者所说，“AI 驱动的形式化证明搜索不仅可以用来解决问题，还能加深人类的理解。”
由于草图是形式化的，专家可以专注于未解决的子目标，而不必从头重新检查整个论证。智能体在捕捉文献中形式化的错误方面也表现出色。“形式化验证可以作为一种过滤器，用于判断哪些证明值得人工审阅，”作者写道。
根据论文，该系统已用于正在进行的量子光学和图论研究中。所有 Lean 证明和选定的自然语言证明都已在 GitHub 上公开。
Erdős 问题成为 AI 数学的基准
OpenAI 最近使用一款专有的推理模型反驳了 Erdős 的单位距离猜想。菲尔兹奖得主 Tim Gowers 称其为“AI 数学的一个里程碑”。在此之前，GPT-5.2 Pro 帮助解决了 Erdős 第 281 号问题，Terence Tao 将此案例称为大语言模型解决开放数学问题“或许最明确的一例”。此后，GPT-5.4 又解决了另一个 Erdős 问题。
从某些角度来看，这些成果比 DeepMind 的方法更令人印象深刻。大语言模型必须通过自然语言承载整个逻辑链条，而没有 Lean 编译器来检查每一步。AlphaProof Nexus 更加系统化且更具可扩展性，但它追求的是不同的目标：为日常数学研究构建一个可靠的 AI 工具。当然，OpenAI 也可以将 Lean 集成到它们的框架中，但关键在于更侧重于测试原始大语言模型能力。
不过，陶哲轩过去曾告诫不要过度解读这些头条新闻。AI 在 Erdős 问题上的实际成功率仅为百分之一到百分之二，而且集中在较简单的题目上。谷歌的系统只解决了 353 个问题中的 9 个。这几乎与陶哲轩所说的百分之二的门槛完全吻合。
没有炒作的 AI 新闻——由人类精选