AlphaProof 9道Erdős题登Science

时间：2026年10月8日（论文在《Science》正式发表）；2026年10月12日 The Decoder 等多家媒体报道 地点：伦敦（《Science》编辑出版地 AAAS）/ 美国加州山景城（Google DeepMind 总部）/ 丹麦奥胡斯（Aarhus University） 人物：DeepMind 团队 20 位作者（第一作者 George Tsoukalas、Pushmeet Kohli、Swarat Chaudhuri 等），合作伙伴 Aarhus University 事件详情：Google DeepMind 与丹麦奥胡斯大学（Aarhus University）联合开发的 AI 数学证明系统 AlphaProof Nexus 正式在《Science》期刊上发表（DOI: 10.1126/science.aej2213，2026 年 10 月 8 日）。这套系统以 Gemini 3.1 Pro 作为底层大语言模型，用形式化证明语言 Lean 起草证明，每一步都由 Lean 编译器逐行检查；编译器返回的错误信息直接喂给模型进行下一轮修订，直到证明通过或系统放弃。论文报告：系统在 353 道已形式化的开放 Erdős 问题中自主解决了 9 道，其中 2 道已悬置 56 年（自 1970 年起）；同时在整数序列在线百科全书 OEIS 的 492 个开放猜想中证明了 44 个；并解决了一道悬置约 15 年的代数几何 Hilbert 函数问题，改进了 min-max 优化中一个已知上界。每个问题的推理成本仅为数百美元。 背景：论文的 preprint（arXiv: 2605.22763）2026 年 5 月 21 日首次提交，6 月 8 日修订；本次《Science》版经过同行评审。AlphaProof Nexus 由四个复杂度递增的 Agent 组成：Agent A 是最朴素的"Gemini 3.1 Pro + Lean 编译器"循环，并行多个子智能体；Agent B 接入 DeepMind 此前在 IMO 拿过银牌的 AlphaProof 子证明工具；Agent C 引入类似 AlphaEvolve 的进化机制，由 Gemini 3.0 Flash 给证明草图打 Elo 评分并按 Plackett-Luce 模型聚合，用作 P-UCB 采样的选择信号；Agent D 是上述能力叠加，被用来攻克 Erdős 问题。研究团队消解测试发现，最基础的 Agent A 也能独立证出全部 9 道 Erdős 题，只是最难的几道花费更高——这意味着"编译器反馈把 LLM 推理锚定在实处"才是整套系统真正的灵魂。 影响：这是 AI 生成的数学证明首次经过《Science》级别的同行评审被正式接收，对学界承认"AI 做了真正的数学研究"具有里程碑意义。同期 Science 的 Perspective 评论文章（Jeremy Avigad 与 Matthew Ballard 撰写）指出"AI 用于科研级数学的时代已经到来"。更重要的是，DeepMind 选择的路径——把证明沉淀到 Lean 代码库、靠编译器而非自然语言自我评估、与人类数学家协同发布——与 OpenAI 近期把数百个 AI 证明倾倒在 GitHub、引发 Terence Tao 领头的"人类数学协会"公开抵制的路线形成鲜明对比。技术层面上，每道题几百美元的推理成本意味着开源问题的"研究成本曲线"再次断崖式下跌，下一步影响将是业余数学家与前沿模型的组合在长尾开放问题上取得突破——本周刚刚发生的"数学爱好者 nor 联手 GPT-6 Astra 一日连破 57 年摆圆 5 题"便是这一趋势的最新注脚。 总结：DeepMind 用 9 道 Erdős 题的《Science》同行评审版本宣告：AI 不仅能解奥数题，也开始能做科研级数学——而 Gemini 3.1 Pro + Lean 编译器这一个最小闭环，就是让这一切发生的全部关键。 参考来源： - Science 论文（AAAS 发布，DOI: 10.1126/science.aej2213）：https://www.science.org/doi/10.1126/science.aej2213 - AAAS 新闻稿（EurekAlert 转载）：https://www.eurekalert.org/news-releases/1146436 - The Decoder 10-12 报道（首发英文媒体）：https://the-decoder.com/google-deepminds-alphaproof-nexus-solved-dozens-of-open-math-problems-and-actually-got-peer-reviewed/ - TSNMedia 详细分析：https://tsnmedia.org/alphaproof-nexus-deepmind-science-9-of-353-erdos-problems-44-of-492-oeis-conjectures - AI Wiki 词条：https://aiwiki.ai/wiki/alphaproof_nexus/revisions/1 - arXiv 预印本：https://arxiv.org/abs/2605.22763 - GitHub 代码仓库（Lean 证明公开）：https://github.com/google-deepmind/alphaproof-nexus-results - 中文报道（科技日报 / 中国经济网）：http://scitech.ce.cn/sy/zx/202610/t20261012_3254497.shtml - 中文报道（Cocoloop）：https://news.cocoloop.cn/zh-tw/2026/10/alphaproof-nexus-science-erdos - 中文报道（IT之家，5月首发）：https://www.ithome.com/0/955/261.htm - 中文报道（量子位转载）：https://news.sig.ai/cn/article/cmpnug2qz0002pfufrs3ss3x4 - 西班牙科学媒体中心评论：https://www.eurekalert.org/news-releases/1146436 - 同行评审 Perspective（Avigad & Ballard）：https://www.science.org/doi/10.1126/science.aej2213