AlphaProof Nexus Erdős 难题进入同行评审，但真正值得关注的是 353 道中的九道
根据 2026 年 10 月 8 日发表于 Science 的一项同行评审研究，Google DeepMind 的 AlphaProof Nexus 在选定的 353 道 Erdős 难题中解出了九道。其中两个问题已悬而未决 56 年。不过，分母与头条本身同样重要：该系统完成了约 2.5% 的选定问题。
AlphaProof Nexus 的 Erdős 难题成果，并不只是又一项宣称 AI 模型能够处理高难度数学问题的成绩。DeepMind 将语言模型生成与 Lean 相结合；Lean 是一种形式化系统，可检查证明中的每一步是否遵循既定定义和规则。团队还发布了可供外部审查的机器可读证明。
这一验证流程使该项目区别于主要围绕自然语言答案构建的 AI 数学实验。不过，它并不能消除人类判断的必要性。数学家仍须确认，每项形式化陈述是否忠实表达了原始问题，以及技术上有效的结果是否确实具有新意。
AlphaProof Nexus 解出九道 Erdős 难题，随后 Science 对这项工作进行了评审
眼前的变化不只是“九”这个数字，而是研究级成果、可由机器检查的产物与传统同行评审的结合。
这项题为“Advancing Mathematics Research with AI-Driven Formal Proof Search”的同行评审研究于 10 月 8 日刊登在 Science 上。更早的一篇研究预印本已于 2026 年 5 月披露了核心发现。
Google DeepMind 的研究人员从 Erdős 问题集里选取了 353 道开放问题，并以 Lean 对其进行表述。据称，AlphaProof Nexus 找到了其中九道的证明。两个问题此前已开放 56 年，为这一结果提供了格外清晰的历史参照。
Paul Erdős 是一位多产的数学家，其提出的问题横跨组合数学、数论、图论及相关领域。与其工作相关的在线问题集包含难度、历史背景和“已解决”定义各不相同的问题。解决其中一道，可能只需要一个被忽略的观察，也可能需要一项全新的研究计划。
因此，这一表现应被理解为：在一个定义明确的测试集中取得九次成功，而不是具备解开任意九个著名猜想的通用能力。实验中，其余 344 道选定问题仍未解决。正是这一边界让研究更具信息价值，因为它同时呈现了成功与失败。
AlphaProof Nexus 还处理了第二个大型基准。研究人员称，它证明了从整数数列在线百科全书中选取的 492 个开放猜想中的 44 个。该数据库已得到广泛认可，将整数数列与公式、观察结果及猜测性质联系起来。
在这些系统性评估之外，该系统还参与了多个研究项目。论文称，它回答了一个有关 Hilbert 函数的开放代数几何问题；还描述了对 min-max 优化中一个界的改进，以及涵盖图论、组合数学和量子光学的工作。
这些额外案例之所以重要，是因为基准分数可能掩盖研究的真实形态。数学家很少会收到数百个格式完美的定理陈述，然后只要求给出完整证明。真实项目往往包含不完整的定义、不确定的中间结论，以及会随着研究人员理解加深而变化的问题。
Science 的发表并不意味着每一项含义都从此尘埃落定。同行评审会评估论文的方法、证据和结论，但并不等同于自动复现每一次计算运行。公开的形式化产物提供了另一层审查，可在发表后持续进行。
DeepMind 的证明仓库包含 Lean 文件和成功证明的自然语言版本。仓库还列出了尝试过的 Erdős 问题，并指向未成功案例的形式化版本。研究人员可以在本地构建该项目，并让 Lean 检查已完成的证明文件。
这项发布让外部数学家获得了比新闻稿摘要更有用的材料。他们可以审查定义，将形式化陈述与原始问题进行比较，并研究哪些证明策略奏效。他们也可以识别某条已有定理是否已经蕴含某项报告中的结果。
公开证据将这一宣布转化为可审计的研究对象。但它不会自动确立数学意义、新颖性或理解深度。这些问题仍属于人类审查流程的一部分。
为什么 AlphaProof Nexus 的 Erdős 难题成果重要
AlphaProof Nexus 将核心问题从“模型能否写出看似合理的数学”转向“智能体能否产出经得起机械与人工检验的证明”。
大型语言模型通过预测文本序列来生成内容，因此能够写出优雅却暗藏细微逻辑错误的论证。在普通文本中，这类错误可能隐藏在数页篇幅里。一个看似自信的结论，可能依赖于此前很早引入的一次无效变换。
Lean 改变了这一工作环境。它是一种证明助手，意味着数学陈述和证明以形式语言写成，其逻辑步骤可由软件检查。一个证明不能仅因听起来有说服力便获通过。
AlphaProof Nexus 将这种严格环境作为主动反馈渠道。语言模型提出 Lean 代码，编译器对其进行评估，错误信息引导后续修改。失败的尝试会成为下一步搜索的信息，而不会作为不可见的推理错误被保留下来。
这种方法类似于编程智能体与编译器、自动化测试协作的方式。模型并不需要每次初始提案都绝对可靠。它需要的是一个能拒绝无效状态、保留有用进展并引导进一步探索的过程。
这一类比也有局限。通过的软件测试套件可能遗漏重要行为，而能够编译的 Lean 证明也可能编码了错误的数学陈述。验证的意义取决于被验证的规格说明是否正确。
这一区别是理解 AlphaProof Nexus 的关键。Lean 确认的是：一个证明是否遵循其接收到的形式化假设。Lean 并不会独立判断这些假设是否符合预期的 Erdős 问题。
形式化是指将普通数学语言转化为证明助手能够处理的定义。量词、边界条件或定义上的细微变化，都可能将一个困难猜想变成较弱的陈述。对这个较弱陈述的证明可以完全有效，却未能解决原始问题。
因此，DeepMind 的工作结合了两种审查形式。机械检查测试内部逻辑有效性；数学家则审查解释、新颖性、相关性，以及形式化定理与其来源问题之间的关系。
这种分层流程对仅依赖自然语言的 AI 研究提出了更高要求。当另一套系统能够提供可执行的形式化产物时，一篇润色精美的证明便不再是最有力的证据。提出数学主张的实验室将面临日益增长的要求，需要发布精确陈述、可由机器检查的证明，以及完整的评估分母。
这一结果也对形式化定理证明器的开发者形成推动。AlphaProof Nexus 表明，通用语言模型在与严格的符号工具连接后可以变得更有用。证明助手提供可靠的局部反馈，而模型则在规模更大、可预测性更低的策略空间中进行搜索。
这种分工的意义超出数学领域。软件工程、硬件设计、安全协议和安全关键系统，都存在可依据形式约束检查生成输出的任务。因此，AlphaProof Nexus 的影响可能远不止其解出的九道 Erdős 问题。
不过，形式化反馈在正确性能够被精确定义时效果最佳。许多商业、科学和社会问题缺乏完整的机器可读规格说明。这种方法无法将每个推理问题都转化为定理证明练习。
更有力的结论其实更为狭窄：当一个领域提供精确验证器时，AI 智能体可以利用失败信号，让长链条推理更可靠。AlphaProof Nexus 为这一设计模式提供了异常具体的证据。
真正的机制是生成、检查与修订
AlphaProof Nexus 之所以有效，是因为每一项提出的证明都必须面对验证器，而不是因为某个模型突然迸发出一段毫不中断的数学洞见。
研究人员研究了四种复杂程度递增的智能体配置。基础版本运行多个子智能体，反复生成 Lean 证明尝试，并根据编译器反馈作出响应。更复杂的配置则加入了专用工具和协调机制。
完整系统在遇到困难子问题时可以调用 AlphaProof——DeepMind 基于强化学习的证明器。AlphaProof 此前是为形式化竞赛数学设计的。在 Nexus 中，它作为更广泛研究工作流中的专注工具发挥作用。
最复杂的智能体还采用了进化过程。多个子智能体探索搜索空间时，候选方法可以被比较、组合和排序。这一结构旨在保留有前景的部分工作，而不强迫每次尝试都经过同一个线性上下文。
这一机制针对了长程 AI 任务中的常见弱点：模型可能放弃有用方法、重复早先错误，或丢失对依赖关系的追踪。对多种尝试进行管理，能增加保留有效分支的机会。
然而，研究得出了一个令人意外的结果。据称，最简单的智能体解出了与完整版本相同的九道 Erdős 问题，而且没有调用专用的 AlphaProof 工具。
这一发现并不意味着更大的框架无关紧要。不同配置在其他任务上的成本和表现各不相同，更先进的系统也帮助处理了某些特别困难的案例。尽管如此，消融结果削弱了任何将头条成果归因于架构复杂性的说法。
它反而凸显了强大的基础模型与毫不妥协的编译器反馈之间的配合。Gemini 3.1 Pro 生成并修订形式化论证，而 Lean 拒绝无效步骤。这个反馈循环提供了普通对话式推理所缺乏的锚定。
研究人员还评估了 OEIS 猜想，系统在 492 个尝试陈述中证明了 44 个。这一更广泛的数据集支持该方法可在多个形式化问题中复现的结论，但并未证明其整体成功率很高。
因此，从操作层面解释 AlphaProof Nexus 很直接。首先，由人类或其他流程将数学问题形式化。接着，多个模型驱动的智能体生成 Lean 代码并接收编译器错误。协调软件将更多工作分配给有希望的证明状态。
最后，成功的形式化证明仍需接受数学层面的审视。研究人员可以将其转述为普通语言，评估其新颖性，并判断它们是否带来有价值的理解。机器检查器减少了一类重要错误，但并不能完成整个科学评估过程。
这种分工也澄清了研究中“自主”的含义。证明搜索可以在无需人类提供每一个中间步骤的情况下进行。人类仍然负责选择问题、准备形式化陈述、配置系统，以及评估完成的输出。
因此，自主性受制于预先准备好的环境。AlphaProof Nexus 并未独立考察整个数学领域、决定哪些问题重要，并在无人监督的情况下发表结论。它是在研究人员提供的任务和工具范围内进行搜索。
这仍然是有价值的自动化。形式化证明开发可能需要围绕引理、表示方式和库组件进行大量试验。即使大多数尝试失败，一个能够探索这些选择并返回可验证候选结果的智能体，仍可为研究人员节省时间。
未成功的搜索也可能暴露出有用的中间事实。一项失败的形式化证明可能揭示缺失的引理、不一致的假设，或一种有前景的重述方式。如果系统能清晰保留这些产物，它们就能支持人类工作。
这正是研究价值可能超越初始得分之处。九项完成的证明会吸引关注，但结构化搜索历史和经过验证的中间步骤，可能成为更重要的科学产出。
形式化验证并不能判定含义或新颖性
Lean 构建成功只能说明编码后的证明有效。它并不能说明该定理是否对应预期问题，或是否带来了新的数学成果。
通过研究者反应发表意见的独立专家指出，形式化是一个核心限制。如果源问题被错误翻译，Lean 仍可能验证一个错误命题的证明。
这并非无关紧要的技术性保留。数学陈述往往浓缩了既定惯例、隐含条件以及对早期文献的引用。形式化版本必须明确每一项相关选择。
这些选择可能改变问题本身。遗漏一个条件可能使定理为假，而额外加入一个假设则可能使其容易得多。人类专家必须将编码后的版本与原始表述及其被接受的解释进行比较。
新颖性还需要另一类调查。一个系统可能为已被早期工作蕴含的陈述给出正确证明。Lean 会检查其环境内的逻辑正确性，但不会检索整个数学文献以确定优先权。
一项独立审计认为，报告的九项结果中有一项已被更早的定理所蕴含。这并不否定相应的形式化证明。它表明，随着专家审查历史文献，新近解决问题的计数可能发生变化。
因此，恰当的表述应当谨慎。论文报告称解决了九个 Erdős 问题，其证明产物也通过了形式化检查。每个案例是否都在最严格的历史意义上构成新的解决方案，仍有待持续审查。
成功率带来了另一项限制。在 353 次尝试中得到九项结果，约占所选集合的 2.5%。这对研究级形式化证明搜索而言具有意义，但并不支持其是通用数学问题求解器的说法。
选择效应同样重要。被尝试的问题必须能够被形式化，并与现有 Lean 库兼容。有些领域更容易表示，因为其基础定义和支撑引理已经以机器可读形式存在。
因此，系统测得的能力反映的不只是推理能力。它还反映了库的覆盖范围、形式化质量、问题选择、可用算力，以及定理与智能体搜索方法之间的兼容性。
成本报告同样需要谨慎。公开描述显示，成功推理运行的单题成本处于数百美元范围。批评者指出，成功运行的数字未必涵盖失败搜索或对专业组件的每一次调用。
如果没有整个尝试集合的总支出，读者就无法计算每个新解决问题的完整成本。仅凭推理支出，他们也无法将该系统直接与数学家的工作进行比较。
人类劳动仍是另一项未定价的投入。专家必须形式化问题、维护库、检查输出、解释发现，并将证明项转化为可理解的论证。即使证明搜索本身是自主的，这些任务也是研究系统的一部分。
基础智能体的表现提出了一个独立的架构问题。如果生成并检查的循环解决了与完整系统相同的 Erdős 问题子集，未来团队就应测试更简单的配置是否能提供可比价值。
更多组件可以改善探索，但也会增加成本，并使故障更难诊断。透明的消融研究至关重要，因为它能识别究竟是哪些机制真正改变了结果。
这些限制并未抹杀这一成就。它们让这项成就得到更准确的界定。AlphaProof Nexus 展示了一种可信的工作流，可产出可检验的研究候选成果，而不是取代数学解释或学术审查。
同行评审改变 AI 数学竞赛
最强的竞争分野不再是一个模型与另一个模型的较量，而是经过验证的发表与将审查成本转嫁给数学家的高产量主张之间的区别。
AI 实验室近来报告了越来越多关于开放数学问题的结果。一些实验室强调模型在自然语言中的原始推理能力。另一些则将模型连接到证明助手、代码执行、符号代数或大型智能体团队。
这些路径优化的是不同目标。自然语言系统可以直接处理研究人员使用的符号和解释风格。它们可能展现出难以在形式化环境中表达的直觉策略。
形式化系统提供更强的局部正确性保证。它们可以立即拒绝无效步骤，并生成其他研究人员可执行的产物。然而，它们依赖于形式化陈述、支撑库和专业知识。
AlphaProof Nexus 将语言模型的灵活性与形式化检查结合起来。随后，Science 论文加入了常规学术审查，让编辑和审稿人有机会质询方法、解释和呈现方式。
这一过程不同于将数百篇 AI 生成的手稿直接发布到公共存储库。大规模发布可能包含有价值的想法，但它们将筛选负担转移给必须判断哪些结果正确、新颖且值得阅读的研究人员。
这篇已报道的论文发表出现在围绕这一负担的激烈讨论期间。数学家警告称，未经检查的结果倾倒可能淹没验证所需的有限人类注意力。
同行评审本身并不能解决扩展问题。期刊同样依赖志愿者或报酬有限的专家。如果 AI 系统生成研究主张的速度超过专家评估它们的速度，传统审查也将面临同样的瓶颈。
机器验证可通过在人类审查前筛除明显的逻辑错误而提供帮助。论文的相关讨论将形式化检查定位为识别哪些证明值得专家关注的方式。这比将验证器视为专家替代品更站得住脚。
因此，竞争优势可能属于那些善于管理注意力的系统。一个有用的数学智能体应当对输出进行排序、揭示假设、追踪依赖关系，并区分已完成的证明与有前景的部分工作。
它还应使负面证据清晰可读。研究人员需要知道哪些策略失败了、哪些引理仍未证明，以及算力花在了哪里。仅有一条打磨完善的最终定理，可能掩盖了大部分有用的研究过程。
对 Google DeepMind 而言，Science 的发表支持了一项以可验证性和选择性披露为中心的战略。公开的 Lean 产物允许技术审查，而同行评审则提供制度性评估。
竞争对手也可以采用相同要素。Lean 是开源的，形式化证明工作流并非某一家实验室独有。持久的优势将取决于模型质量、搜索效率、库深度，以及与一线数学家的整合程度。
大学面临一个资源问题。针对数百个研究问题运行前沿模型，可能需要大量算力和工程支持。如果只有大型实验室能够有效运行这些系统，自动化发现的获取机会可能变得不均衡。
开放的证明产物部分缓解了这种不平衡。无法运行原始智能体的研究人员，仍可检查成功证明、测试形式化陈述，并在已发布成果之上继续构建。他们未必能够复现整个搜索过程。
因此，竞争的下一阶段应通过可复现性来衡量，而不应只看头条数字。实验室需要披露尝试集合、算力核算、人类干预、形式化流程，以及独立检查的状态。
AlphaProof Nexus 之后值得关注什么
三个信号将决定 AlphaProof Nexus 是否成为持久的研究工具：外部审计、更简单智能体的复现，以及持续人机协作的证据。
第一个信号是对九项 Erdős 结果进行独立数学审查。专家应将每个 Lean 陈述与源问题进行比较，审查既有文献，并评估每项证明的解释价值。
如果大多数结果经这一过程证明是忠实且新颖的解决方案，核心主张就会更有力。如果其中若干项被重新分类，形式化搜索仍具有技术价值，但头条计数的意义会减弱。
公开文件使这种审查成为可能。每个成功产物都可以被构建、检查，并与自然语言论证建立联系。未来的存储库更新可能会揭示更正、改进后的解释，或对个别问题描述方式的变化。
第二个信号是独立团队能否用更简单的系统复现可比结果。基础智能体在同样九个 Erdős 问题上的成功表明，直接的模型与编译器交互完成了大部分关键工作。
复现应比较总算力、失败运行、库准备和研究人员时间。更廉价的生成—检查—修订循环将加强广泛采用的理由。如果在 DeepMind 之外无法成功，则表明隐藏基础设施或实现选择比论文所暗示的更为重要。
研究人员还应测试 344 个未成功形式化的问题。相较于反复解决最初的九个问题，在这些问题上的改进将提供更清晰的进步衡量。这一未解决集合构成了一个具有既定基线的高难度公共基准。
第三个信号是数学家在真实研究中持续使用。完成基准很有用，但科学价值取决于智能体是否能帮助人们构建定义、发现引理、检验猜想，以及理解意外出现的结构。
最有说服力的部署将记录研究人员与系统之间的互动。读者应能看到人类提供了什么、哪些机器建议改变了项目，以及验证如何影响最终论证。
一批不断增加、已获认证却缺乏可理解解释的结果，也会带来另一类问题。数学重视证明，不仅因为它是正确性的凭证，也因为它是传递洞见的方法。
如果 AlphaProof Nexus 的输出能够帮助研究者形成新概念，或连接此前彼此分离的想法，其影响将更为深远。一份只有编译器能够读懂的证明，或许可以确立某个命题，却未必能以同样的速度推动人类理解。
该系统的意义同样延伸至数学之外的智能体开发者。其核心模式很明确：将概率式生成与精确评估器连接起来，保留有价值的中间状态，并将人工审查留给通过初步检查的输出。
这一模式可以改进代码生成、硬件验证、协议设计，以及其他具有严格规范的领域。但它无法保证规范本身准确捕捉了用户真正想实现的目标。
对于知识工作者而言，这正是实际启示：验证必须匹配任务的正确层级。自动化检查可以确立一致性，但相关性、意图、新颖性以及后果仍需由人来判断。
因此，AlphaProof Nexus 的 Erdős 问题故事，既不是自动化数学至高无上的宣言，也不只是一次小幅度的基准测试更新。它证明，AI 证明搜索能够以有意义的规模产出可审计的研究候选成果。
下一个问题是，围绕它的研究流程能否同步扩展。请关注公开审计、其在此前尚未解决的形式化问题上的表现，以及数学家明确报告获得真实理解提升的合作案例。这些信号将表明，经过验证的 AI 推理究竟会成为科学基础设施，还是仍只是一场令人印象深刻的实验室展示。
