北大团队的探索：AI解决数学猜想的新突破北京国际数学研究中心BICMR
近期，北京大学北京国际数学研究中心（BICMR）董彬课题组与合作者（至知创新研究院等）组建的AI4Math团队宣布：他们构建的自动化AI框架解决了交换代数中一个开放问题Anderson 猜想，并在Lean 4中完成了约19,000 行的形式化验证。这背后，是一支扎根北大数学的团队三年的积累。
北京国际数学研究中心办公院落内景
2021 年，DeepMind 在Nature发表了一项引人注目的工作“Advancing mathematics by guiding human intuition with AI”，展示了AI如何辅助数学家发现新的数学规律。该论文不仅在数学界引发了广泛关注，也吸引了北京国际数学研究中心众多老师的目光。
2022 年初，在刘若川和肖梁两位教授引荐下，董彬教授课题组开始与时任香港中文大学教授何旭华合作，用机器学习分析一类代数几何对象（仿射Deligne-Lusztig簇）。研究不仅“重新发现”了已知的维数公式，更在当前理论相对薄弱的边界区域检测到系统性偏差，并据此证明了新定理。相关成果于2024年发表在Peking Mathematical Journal上。这是团队第一次看到AI捕捉到人类尚未注意的数学规律。
B. Dong, X. He, P. Jin, F. Schremmer, Q. Yu, Machine learning assisted exploration for affine Deligne-Lusztigvarieties, Peking Mathematical Journal, 2024
2023 年初，大语言模型快速发展。正在深入探索机器学习的董彬开始思考：AI 能否更全面地参与数学研究？当时不少同行觉得这是天方夜谭，但在他看来值得全力一试。他的判断是：必须把自然语言推理与形式化验证结合起来——前者在已有文献中搜索线索、构造证明思路，后者将思路转化为可被计算机逐行检查的形式化代码。这个思路延续至今。（相关思考可参见AI for Mathematics：数学智能副驾驶的构想）
董彬的思想获得了同事们的认可和支持，北京大学AI4Math团队随即组建：刘若川、肖梁、文再文、董彬四位教授分别来自代数与数论、优化、机器学习与人工智能方向，成员涵盖本科生到研究人员。与当时多数团队聚焦数学竞赛不同，这支团队从一开始就以推动数学科研为目标，并有意选择代数方向的开放猜想作为主攻方向。基础数学家把握问题本质，应用数学家搭建算法和系统——北大数学在多个基础方向的长期积累，为这种深度协作提供了土壤。
基础设施：检索是核心
要让AI 做严肃的数学推理，需要检索、推理、数据、评测一整套基础设施。团队认为其中检索最为关键，尽管它常常被低估。面对一个新问题，找到正确的切入点——哪个方向的理论工具或视角可能对当前问题有帮助——往往是最需要数学智慧的一步。数学知识分布在众多子领域中，跨方向的关联隐而不显，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 猜想正是肖梁为团队选定的一系列目标之一。
这个被解决的开放问题，收录在《交换环论中的开放问题》（Open Problems in Commutative Ring Theory）中，由美国爱荷华大学数学家 D.D. Anderson于2014 年提出。正如肖梁所指出的，该问题关注的是“准完备局部环”的一类性质——这类环旨在用代数工具刻画几何对象局部（如某点附近）的无穷小结构与变形，属于交换环论这一代数分支中的基础性开放问题。具体而言，满足某种“弱”逼近性质的 Noetherian局部环，是否自动满足更强版本的同类性质？这类问题在数学中反复出现——弱条件和强条件之间的差距，往往藏着意想不到的构造。该猜想提出后始终无人突破，构造反例所需的技术工具分散在不同子领域中，难以被同一位研究者同时掌握。
Rethlas通过Matlas在上千万条数学陈述中检索，从一个看似无关的方向——关于整环完备化的理论——定位到了Jensen（2006）的一个技术性结果。Jensen的工作本身与Anderson问题无关，但Rethlas发现它恰好提供了构造反例所需的工具，并据此给出了否定回答：弱条件不蕴含强条件。这种跨方向的精准定位，正是数学研究中最依赖不同领域专家之间深入交流才能实现的。
Archon 随后将证明转化为约 19,000 行Lean 4代码。形式化不是翻译——论文中每一个“显然”，在Lean 4中都必须严格展开。Archon做了两个自主决策：其一，发现初始方案存在隐含的逻辑漏洞，主动推翻原方案，重新设计了形式化证明的整体技术路线；其二，发现所需的一个数学概念在Mathlib 中尚未收录，自主找到一条等价的替代路线绕过障碍。最终代码覆盖了6 篇外部论文的关键结果。相比一位经验丰富的Lean专家，Archon完成同等规模形式化工作的效率至少提升了 10 倍。
新突破振奋人心。正如刘若川所说，“这让我们看到了数学与AI深度融合的一种可能。数学家们需要关注的不仅是某个具体问题是否被解决，更是这种新的研究范式能否持续产出、能否培养出新一代既懂数学又能驾驭 AI 工具的年轻研究者。董彬团队这几年的探索，从工具搭建到问题攻克，走出了一条有说服力的路。期待AI4MATH方向能吸引更多优秀的年轻人加入，北大数学有信心有条件为他们提供成长的土壤。”
值得一提的是，这项工作的组织方式本身就不寻常。北大AI4Math团队不是由某个具体项目牵引组建的，而是一群对这个方向有共同判断的人逐步自然汇聚而成。这种“自发有组织”的科研模式在国内并不多见，它的形成也离不开学校和院系的大力支持。
“自发有组织”的团队模式拥有独特的理想主义氛围，同时也要面对现实的压力和挑战。对外，AI 技术日新月异，学界和业界的竞争激烈且充满不确定性——什么时候该坚持、什么时候该调整，每一个战略判断都关系到整个团队的方向，压力和焦虑始终相伴。对内，团队成员来自不同的数学分支和计算机方向，学术背景、个人诉求和价值取向各不相同。要让大家拧成一股绳，需要不断沟通、鼓劲，也要说服年轻人敢于跳出现有评价体系的框框，去做真正有长远价值的研究。
田刚院士指出，“由董彬与刘若川、肖梁等教授组成的北大AI4Math团队以AI框架攻克交换代数的一个开放问题，并完成大规模形式化验证，在国内尚属首次，具有重要的示范意义。此次成果展现出北大数学有活跃的学术生态，北大年轻数学人有极大的创新活力。我希望给予青年学者更多的平台，鼓励和支持他们大胆创新，勇于探索，进一步推动人工智能与数学的深度融合，取得更多具有国际影响力的突破性成果，并在国家急需解决的科技重大问题中发挥关键作用。”
在AI4Math这样的前沿方向，与包括企业在内的社会团体的紧密协作是团队保持在技术前沿的关键之一。在此，团队特别感谢与至知创新研究院（IQuest Research）在算力、资源与技术方面的紧密合作，以及新基石科学基金会对基础研究的长期资助。
往前看，AI 与数学的交汇至少有三个层面值得期待：构建并借助AI 工具去挑战越来越难的数学问题，不断推高研究的天花板；研究AI本身——数学为理解和改进AI提供了独特视角，有望推动更经济、更安全、更可解释的 AI 系统的发展；运用数学思维去驾驭AI，将它应用到科学和工程中同样深刻的问题上。可能性才刚刚打开。
目前，两个智能体的基座模型主要基于国外的大语言模型。团队期待未来能与国内头部基座模型团队开展更深入的协作，共同推动这一方向的发展。
