Google DeepMind 的 AlphaProof Nexus 解决数十个开放数学问题并通过同行评审
Google Deepmind's AlphaProof Nexus solved dozens of open math problems and actually got peer reviewed
Google DeepMind 的新研究显示，AlphaProof Nexus 自主解决了 353 个 Erdős 开放问题中的 9 个，其中两个已悬置 56 年，相关解法在论文发表前已公开。该系统还证明了 OEIS 整数序列数据库中的 44 个猜想，解决了代数几何中的一个开放问题，并改进了 min-max 优化中的一个已知界。它基于 Gemini 3.1 Pro，用形式化语言 Lean 起草和修订证明，Lean 在每次修改后检查草稿，错误信息引导下一次尝试；遇到更难的子问题时还可调用专用证明工具 AlphaProof，但即使不调用 AlphaProof 也能解决那 9 个 Erdős 问题。该研究发表在 Science 上，并经过了同行评审，而 OpenAI 近期将数百个 AI 证明直接发布到 GitHub 而非提交期刊，由 Terence Tao 领导的 Association for Human Mathematics 呼吁抵制。
推荐理由
精选AI 评分 88
AlphaProof Nexus 用 Lean 形式化验证并接受同行评审，与 OpenAI 直接公开证明的做法形成对照。
主题
正文
当前显示原文，中文全文译文尚未就绪。
Google Deepmind's AI solved dozens of open math problems on its own, per a new study in Science . AlphaProof Nexus cracked nine of 353 open Erdős problems, two unsolved for 56 years. The team shared those solutions online ahead of the paper.
Beyond that, AlphaProof Nexus proved 44 conjectures from the OEIS integer sequence database, solved an open question in algebraic geometry, and improved a known bound in min-max optimization, a technique used to train some AI models. It's built around Gemini 3.1 Pro, which drafts and revises proofs in the formal language Lean. Lean checks each draft after every edit, and error messages guide the next attempt. For harder sub-problems, it can call on AlphaProof , a specialized proof tool. Even without AlphaProof, it solved the nine Erdős problems, Google Deepmind reports .
The study lands amid a heated debate over AI math. OpenAI recently dumped hundreds of AI proofs on GitHub instead of submitting them to journals. The Association for Human Mathematics, led by Terence Tao, called for a boycott . Deepmind put its work through peer review.