AI解决数学猜想的新突破!至知创新研究院联合北大团队的探索

2026年4月，北京大学 AI4Math 团队宣布，联合至知创新研究院等合作伙伴，利用自主构建的 AI 框架首次解决了交换代数中的 Anderson 开放问题，并在Lean 4 中完成了约 19000 行的形式化证明验证。这一成果是国内首次以 AI 框架解决数学开放问题并进行大规模形式化验证，标志着数学与人工智能深度融合进入了全新阶段。

至知创新研究院作为该项目的重要合作方，从2024年起便与北大国际数学研究中心紧密协作。此次合作，整合了北大团队在开创性数学问题上的突破经验与至知团队在AI系统研发与工程化落地方面的优势，共同推动数学领域的前沿创新。

至知创新研究院在数学智能方向构建了完整的科研体系，与北京大学国际数学研究中心围绕形式化数学证明与自动推理形成了从数据构建、模型训练到工具开发的全链条布局。合作团队联合发布了 FATE (Formal Algebra Theorem Evaluation) 系列评测集。以大学-猜想级别抽代为主，为数学推理能力的标准化评估提供了重要基准。该系列成果已发表于 ICLR 2026，为数学推理能力的标准化评估提供了重要基准。值得注意的是，研究团队还开源了 FATE 及其评测代码，为推动国内数学人工智能研究建立统一评测基准。在核心工具开发层面，至知创新研究院联合北京大学推出了 LeanSearch，达到 SOTA 级别的 Lean 引理检索能力，有效支持复杂数学证明中的引理查找需求，同时开发了 Lean Copilot (MoZi)，作为支持 Lean 的辅助证明能力的 VS Code Copilot 插件，将大模型能力直接嵌入形式化证明的交互流程中，提升证明开发的效率与体验。在自动形式化方向，训练了 Agentic 的 Autoformalizer 模型，在数学语言与自然语言之间的自动翻译任务上达到业界 SOTA 水平，为数学知识的结构化转化与自动化处理提供了关键技术支撑。通过上述工作，在数学智能领域形成了涵盖评测标准、检索工具、交互插件与翻译模型的完整技术矩阵，推动了形式化数学与人工智能的深度融合。

上述工作构建了从检索、推理、数据、评测一整套基础设施。

基础设施：检索是核心

面对一个新问题，找到正确的切入点——哪个方向的理论工具或视角可能对当前问题有帮助——往往是最需要数学智慧的一步。数学知识分布在众多子领域中，跨方向的关联隐而不显，AI 必须先找到相关的理论和文献，才能开始构造证明。

形式化验证依赖 Lean——一种证明助手，数学家写下的每一步推导都会被 Lean 内核逐行检查。支撑 Lean 的是 Mathlib，一个包含数十万条定理和定义的形式化数学库。团队在这个方向上几乎是从零起步：成员们先自学 Lean，再逐步在国内组织课程和研讨班，推动形式化数学的普及。在此过程中，团队深刻体会到一个核心瓶颈：AI 如何从 Mathlib 数十万条定理中快速找到所需的那一条？为此，团队构建了 LeanSearch，用自然语言描述需求即可语义检索出相关定理，现已被 Lean 官方社区广泛使用，API 日均调用超过 8000 次。

自然语言文献一侧同样面临检索瓶颈。团队构建了 Matlas，覆盖上千万条数学陈述，支持命题级语义检索。LeanSearch 覆盖形式化世界，Matlas 覆盖自然语言世界——这种双引擎架构是该框架区别于其他 AI 数学系统的核心特色。

两个智能体

在上述基础设施之上，团队搭建了两个协作的 AI 智能体，均基于现有基座模型构建。

Rethlas 负责自然语言推理——搜索文献、构造证明方案、试错修正。它模拟数学家的工作方式：提出猜测、尝试构造、遇到矛盾后回溯调整，在多轮试错中逐步逼近可行的证明路径。

Archon 负责形式化验证——将自然语言证明转化为 Lean 4 代码并补全所有细节。Archon 此前已开源，在研究级基准测试中验证过形式化能力。

团队围绕数学研究为两个智能体构建了一整套能力：从数学家的研究实践中提炼出的推理策略和证明规划方法，从数十万条形式化定理和上千万条自然语言陈述中精准检索的能力，以及面对基础设施缺失时自主寻找替代路径的机制。这些能力的背后，是北大数学团队对 “数学研究究竟需要什么” 这个问题的长期思考而形成的深刻理解。

Rethlas-Archon协作流程示意图

什么是 Anderson 问题

Anderson 问题关注的是 “准完备局部环” 的一类性质——这类环旨在用代数工具刻画几何对象局部（如某点附近）的无穷小结构与变形，属于交换环论这一代数分支中的基础性开放问题。具体而言，满足某种“弱”逼近性质的 Noetherian 局部环，是否自动满足更强版本的同类性质？这类问题在数学中反复出现——弱条件和强条件之间的差距，往往藏着意想不到的构造。该猜想提出后始终无人突破，构造反例所需的技术工具分散在不同子领域中，难以被同一位研究者同时掌握。

Rethlas 通过 Matlas 在上千万条数学陈述中检索，从一个看似无关的方向——关于整环完备化的理论——定位到了 Jensen(2006) 的一个技术性结果。Jensen 的工作本身与 Anderson 问题无关，但 Rethlas 发现它恰好提供了构造反例所需的工具，并据此给出了否定回答：弱条件不蕴含强条件。这种跨方向的精准定位，正是数学研究中最依赖不同领域专家之间深入交流才能实现的。

Archon 随后将证明转化为约 19,000  行 Lean 4 代码。形式化不是翻译——论文中每一个“显然”，在 Lean 4 中都必须严格展开。Archon 做了两个自主决策：其一，发现初始方案存在隐含的逻辑漏洞，主动推翻原方案，重新设计了形式化证明的整体技术路线；其二，发现所需的一个数学概念在 Mathlib 中尚未收录，自主找到一条等价的替代路线绕过障碍。最终代码覆盖了 6 篇外部论文的关键结果。相比一位经验丰富的 Lean 专家，Archon 完成同等规模形式化工作的效率至少提升了 10 倍。

愿景与展望

数学是基础科学的基石，在人类认知体系中具有核心地位。我们相信，大型语言模型 (LLM) 在数学证明方面的探索，既能拓展人类攻克高难度数学问题的能力，也有望推动数学研究从以人为中心向 “人机协同” 乃至 “机器主导” 的自动化发现阶段演进，成为继公理化、计算化之后的又一次范式飞跃。站在人工智能浪潮之巅，至知创新研究院致力于破解前沿研究与广泛应用之间的核心难题。我们并非传统的学术机构或单纯的实验室，而是一个深耕产业实战的新型科研组织。我们的使命明确而笃定：以前沿的原创性研究为基石，系统加速 AI 技术在数学推理、生物医药、物理材料等关键领域的深度融合与价值创造。我们持续攻坚下一代 AI 基础架构，追求更高效、更可靠的模型与计算范式；同时积极推动 AI 与科学的交叉创新，让人工智能真正成为新时代数学研究的新引擎。

在此特别感谢北京大学国际数学研究中心董彬教授团队的深入合作与支持。

至知创新研究院将继续携手包括北京大学在内的更多高校和科研院所，围绕智能与关键领域的赋能与结合而深入探索，为实现 “人工智能助力科学突破” 这一愿景不懈努力。

文中重点介绍的关于解决 Anderson 猜想的报告、结果和开源工具链接如下：

技术报告：https://frenzymath.com/blog/conjecture/

Rethlas开源：https://github.com/frenzymath/Rethlas

Archon开源：https://github.com/frenzymath/Archon