想象你在解一道没有标准答案的难题。每走一步，都有许多岔路；走错几十步后才发现漏洞，前面的努力便可能白费。AI 做数学证明也面对同样的问题。不同之处在于，它现在可以把每一步交给一个绝不通融的检查员验算，再根据报错继续找路。
这正是 George Tsoukalas 等人发表于 Science 的研究所做的事：让 AI 驱动的形式证明搜索从竞赛题走向开放研究问题。所谓形式化证明，就是把定理、前提和每一步推理写成计算机能严格检查的语言。它像一份必须成功“编译”的证明书，可以挡住那些听起来合理、实际上藏着漏洞的论证。
AI 猜路，Lean 把关
据 Science/AAAS 新闻稿，研究团队开发了 AlphaProof Nexus。系统安排多个 AI 子智能体同时寻找证明，并依据 Lean 编译器的反馈调整方向。Lean 是一种交互式定理证明器：人或 AI 提交证明步骤，它按照预先声明的公理和定义逐步核验。
这里的关键不是让语言模型一次写出漂亮答案，而是把证明变成可以反复试错的搜索。证明通常有大量可能的下一步。语言模型负责提出看起来有希望的路线，Lean 则负责判定这些步骤在形式逻辑上能否成立。增强版本还使用进化算法协调不同子智能体，并可调用 AlphaProof 作为专门的证明工具。
这个分工很重要。大模型擅长生成候选方案，却可能把错误说得很流畅；形式化系统不负责灵感，但能逐步验算。两者组合，相当于让一群解题者不断交卷，再由一位只认规则的检查员即时退回错误步骤。
从练习题走向开放问题
新闻稿称，团队尝试了 353 道开放的 Erdős 问题，系统自动解决其中 9 道；两道问题已经开放超过 50 年。Erdős 问题是数学家 Paul Erdős 提出或传播的一批开放问题。它们不是为考试准备的已知题，而是此前没有公认解答的研究问题。
系统还证明了 492 个开放 OEIS 猜想中的 44 个。OEIS 是收录整数数列及其规律的公共数据库，其中一些猜想可以写成适合机器检查的明确命题。新闻稿还称，这套系统被用于组合数学、优化、图论、代数几何和量子光学等研究。
成本也开始进入可讨论的范围。论文预印本和出版方摘要页称，每道成功解决的 Erdős 问题，推理成本约为数百美元。一个只在大模型生成与 Lean 验证之间循环的基础版本，也复现了这 9 项结果，不过处理最难的问题时成本更高。
为什么这次值得关注？
变化不只在于“AI 又多做对几道题”。更值得看的是任务边界：研究者把形式证明搜索用于真实的开放问题，并给出了可以由证明器逐步检查的结果。形式验证让结论不必只依赖模型的表达是否可信，也为人类复核提供了明确对象。
Science 在 2026 年 10 月第 394 卷第 6820 期集中刊发了这篇论文和两篇评论。Jeremy Avigad 与 Matthew Ballard 的评论标题直接宣称“用于研究数学的 AI 已经到来”；Emily Riehl 的标题则提醒，AI 虽已解决许多数学问题，却还没有“解决数学”。这组并置恰好划出了当前进展的边界：工具已经进入研究现场，但“能证明一些命题”和“能承担数学研究”并不是一回事。
论文最初于 2026 年 5 月发布预印本，同行评审版本于 10 月 8 日刊登在 Science，DOI 为 10.1126/science.aej2213。
离“解决数学”还有多远？
- Lean 检查通过，代表证明在给定公理和定义下形式成立；它不自动说明这个定理重要，也不说明证明提供了新的数学洞见。
- 353 道 Erdős 问题解决 9 道、492 个 OEIS 猜想证明 44 个，说明系统已能处理部分开放问题，但材料没有提供足够信息判断这些问题的代表性，也没有独立复现证据。
- “AI for research mathematics has arrived”是同期评论的概括性判断，不等于 AI 已能自主选择重要问题、形成研究方向或达到人类数学家的整体能力。更稳妥的说法是：AI 形式证明搜索已经跨入真实数学研究，但它跨过的是应用场景的门槛，不是数学本身的终点。