精选理由
数学研究者和 AI 爱好者会兴奋——AlphaProof Nexus 用数百美元成本就解决了人类 56 年未解的难题，证明 AI 已能自主推进数学前沿，值得点开看看具体怎么做到的。
谷歌 DeepMind 推出 AlphaProof Nexus，结合大语言模型与 Lean 形式化验证，在 353 个开放的 Erdős 问题中自主解决 9 个，包括 2 个悬而未决 56 年的问题。该系统由 4 个复杂度递增的 AI 智能体组成，每个问题推理成本仅数百美元。研究还发现，最简单的 Agent A 也能证明这些难题，反映出底层模型能力提升和编译器反馈的锚定作用。这标志着 AI 在数学研究领域取得重大突破，能自主发现并证明长期未解猜想。
AI 翻译 · 中文
谷歌 DeepMind 推出 AlphaProof Nexus，结合大语言模型与 Lean 形式化验证，在 353 个开放的 Erdős 问题中自主解决 9 个，包括 2 个悬而未决 56 年的问题。该系统由 4 个复杂度递增的 AI 智能体组成，每个问题推理成本仅数百美元。研究还发现，最简单的 Agent A 也能证明这些难题，反映出底层模型能力提升和编译器反馈的锚定作用。这标志着 AI 在数学研究领域取得重大突破，能自主发现并证明长期未解猜想。
IT之家 5 月 26 日消息，谷歌 DeepMind 最新推出 AlphaProof Nexus，结合大语言模型（LLM）生成证明与 Lean 形式化验证， 在 353 个开放的 Erdős 问题中自主解决 9 个，并解开 2 个悬而未决 56 年的问题。 IT之家注：Lean 是一种形式化证明语言和证明助手系统。研究者可以把数学命题、定义和证明步骤写成严格可检查的代码，编译器会逐步判断每一步是否合法。 Erdős 问题（Erdős …