北大重大突破！AI 成功攻克多年悬而未决的数学猜想，AI 数学研究迈入新阶段

luyuanhong

北大重大突破！AI 成功攻克多年悬而未决的数学猜想，AI 数学研究迈入新阶段

原创  CC  CC 陈老师  2026 年 10 月 1 日 12:30  湖北

2026 年，北京大学北京国际数学研究中心对外公布重磅成果，董彬教授带领的 AI4Math 团队，利用自研双智能体框架，成功解决交换代数领域的安德森猜想，并且在定理证明工具 Lean 中完成一万九千行左右的形式化验证。这也是国内首次依靠 AI 框架攻克遗留数学开放猜想，消息在国际数学界和 AI 科研圈掀起巨大反响。

安德森猜想早在 2014 年提出，十余年间，全球众多数学家持续研究，始终没有找到完整证明或反例。本次研究团队搭建两套协同智能体，Rethlas 智能体负责检索海量数学文献、构建推理思路，找到看似无关的理论成果构造反例；Archon 智能体则把自然语言的推导过程，转化成严谨、可核验的形式化证明代码，每一步逻辑都能被机器校验，杜绝人为证明里容易出现的逻辑漏洞。

很多人会疑惑，AI 这次突破，是不是意味着机器可以取代数学家做原创研究？参与项目的学者给出客观解读。这次 AI 是在已有数学知识库的基础上完成推理，能帮助数学家快速检索文献、验证推导思路，减少大量重复推演工作，但提出猜想、确定研究方向，依然依靠人类数学家的洞察力。AI 擅长在已有理论体系内寻找逻辑链条，暂时无法独立开辟全新的数学分支。

这项成果对于数学教育同样具备深远意义。过去数学证明教学最大难点，就是学生很难判断证明步骤是否严谨。形式化证明工具未来有望走进高校数学系课堂，学生书写的证明过程可以实时核验，精准定位逻辑断层，改变过去只能依靠教师人工批改证明题的模式。不少高校数学教师提出，未来可以借助这套思路开发教学工具，训练学生严谨书写推理过程。

当然这项技术落地还有很长的路要走。目前这套框架只能针对特定代数领域的猜想，通用性有限，面对几何、分析等其他方向的复杂数学问题，还难以独立完成突破。而且模型高度依赖高质量数学文献数据库，遇到表述模糊、缺少前置理论的问题，依旧容易出错。

长期以来，大众对 AI 解数学题的印象，大多停留在中小学习题、大学计算题。北大这次成果，刷新了大家对 AI 数理能力的认知：AI 不再仅仅用来算答案，已经可以参与前沿数学猜想的探索与严谨证明。

基础数学是所有理工科、人工智能技术的底层根基。AI 和纯数学双向赋能，一方面 AI 加速数学猜想验证，另一方面数学的严谨逻辑持续优化大模型推理能力。未来，数学家与 AI 智能体协同开展研究，将成为基础科研的全新范式。而对于各级数学教育来说，教会学生看懂逻辑、核验推理，将成为新时代数学学习的核心任务。

CC 陈老师