谷歌旗下“深度思维”（DeepMind）团队开发了一种名为AlphaProof Nexus的AI框架，可自主搜索数学证明，并通过Lean等形式化证明工具验证推理过程。相关成果于2026年10月8日发表在《科学》期刊上。

近年来，AI在数学推理方面能力提升明显，但竞赛数学主要考查已有方法的灵活运用，大模型容易产生逻辑错误，难以直接用于严谨的数学研究。为此，研究团队将大模型生成与形式化验证相结合：AI先用Lean语言起草证明，再由编译器逐行检查每一步是否符合数学公理和规则；若发现错误，系统会根据反馈调整证明，直至通过验证。

测试显示，该系统在353个厄多斯开放问题中自主解决了9个，其中两个问题已悬置56年；同时证明了《整数数列在线百科全书》492个开放猜想中的44个，并处理了代数几何、优化、量子光学和图论等领域的多个科研级问题。研究团队还发现，即便只保留基础大模型和Lean反馈循环，该系统也能解决上述9个厄多斯问题，只是在处理更难题目时需要更多计算资源。

信息来源：

https://www.science.org/doi/10.1126/science.aej2213

https://www.stdaily.com/web/gjxw/2026-10/12/content_593883.html