发布
2026 年 10 月 8 日,《科学》(Science) 刊发了 Google DeepMind 关于 AlphaProof Nexus 的同行评审论文。系统使用 基于大模型的智能体,在 Lean 中搜索数学证明,Lean 会由计算机 机械地验证 每一步。
成果
- 在尝试的 353 个埃尔德什问题中自主解决 9 个(约 2.5%),其中 两个悬而未决 56 年(1970 年埃尔德什与沙尔克齐提出的 #12(i)、#12(ii)),每题推理成本 数百美元
- 证明了 OEIS 492 个猜想中的 44 个
- 解决了关于 希尔伯特函数的 15 年老问题,改进了 凸优化 中的界,并发现文献中的 形式化错误
证明公开于 GitHub google-deepmind/alphaproof-nexus-results(Apache 2.0)。
原理
- 智能体 A: 简单循环,大模型(Gemini 3.1 Pro)生成,Lean 验证,错误反馈给模型
- 智能体 D: 由 进化算法 协调的子智能体,可调用 AlphaProof
关键保留意见
事后分析显示,简单循环的智能体 A 解出了同样的 9 个问题(最难的题成本更高)。Josep Curto(UOC)认为关键在于 强大的大模型加严格的验证器反馈,并批评成本只统计成功运行。
此外,Lean 并不能消除幻觉(只保证形式化命题);样本是已形式化的问题,并非随机;Javier Aramayona(ICMAT)等人担忧出现 被证实却无人真正理解的结果。
数学之外的意义
"生成—验证" 模式适用于任何 AI 智能体:
- 没有自动验证就不要信任输出(测试、校验器)
- 从简单开始
- 核对需求规格
- 包括失败在内 衡量总成本
来源
- Science, doi 10.1126/science.aej2213 (8/10/2026)
- arXiv 2605.22763: https://arxiv.org/abs/2605.22763
- GitHub, google-deepmind/alphaproof-nexus-results: https://github.com/google-deepmind/alphaproof-nexus-results
- Science Media Centre Spain: https://www.sciencemediacentre.es/en/alphaproof-nexus-new-ai-tool-designed-tackle-mathematical-proofs
- postcutoff: https://postcutoff.com/e/2026-10-08-alphaproof-nexus-science-paper/
想在业务中引入带自动验证的 AI 智能体吗?KGA IT 提供免费咨询:kga-it.com