在北大,数学家用AI做啥题?

人工智能将改变科学研究的范式。这个过程如何发生？其中的人会经历怎样的酸甜苦辣？北大数学有一群人正在为我们展开这样的故事。

“如果若干年后数学真的被AI改变了，我会记得在燕园，始作‘勇’者是你——董彬。”

肖梁有一次在怀新园院子里对董彬说了这番话。话里有调侃，也有一层说不清的意味。因为当时没有人确切知道他开启的这件事最终会走向哪里，是不是好事。

但为什么还要做？董彬的回答很直接：“如果数学真的会发生变化，我们要在第一线，站在最前面见证这个过程，最好是参与其中，这样下一步怎么走才心中有数。”

Nature网站及专题报道截图

2026年5月，北大AI4MATH团队交出了一份答卷。他们牵头研发的AI系统Rethlas-Archon，在全自动、无人类参与的条件下，通过构造反例否定了交换代数领域悬置十余年的Anderson猜想，并完成近两万行Lean 4形式化验证（即让计算机逐行检查证明的每一步）。Nature杂志2026年5月21日的专题报道“AI is transforming mathematics. Will it conquer the field?”提到了本次工作，将其作为当前AI与数学深度融合的前沿案例加以介绍。

怀新园是北京国际数学研究中心办公院落之一，这个位于燕园未名湖北畔的学术机构成立于2005年。创始主任田刚院士悉心培育这里的科研土壤，十多年来看着一个又一个年轻人挑战大问题，挑战无人区，并一次又一次迎来胜利的曙光。他为北大AI4MATH团队交出的答卷感到高兴和振奋。

这是一个关于几位青年教授、一群学生和一个看起来“不太可能”的方向的故事。它开始于2021年。

文再文、刘若川、董彬、肖梁合影

四种动机，一个方向

2021年，DeepMind（谷歌旗下AI研究机构）在Nature发表了一篇论文，展示AI如何辅助数学家发现新规律。北京国际数学研究中心的几位老师注意到了。当时，数学圈里多数人的反应是：有意思，但跟我关系不大。“早期讲AI for Math的时候，很多老师都觉得，AI可能给我提供了一个计算器，提供了一个小工具。没有多少人会认为这个东西有可能会改变我们的做事方式。”董彬回忆。

董彬的判断不一样。他看到的不是一个工具，而是一种可能性。2022年初，经刘若川和肖梁引荐，他的课题组与香港中文大学何旭华教授合作，用机器学习分析仿射Deligne-Lusztig簇（一种与李代数、p进群表示论相关的几何对象），在边界区域检测到系统性偏差并证明了新定理，相关成果后来发表在数学期刊Peking Mathematical上。

Peking Mathematical 论文截图

这是团队第一次主动用AI捕捉到人类尚未注意的数学规律。这次合作让董彬确信方向是对的，但工具还不够。

到2023年，大语言模型横空出世，董彬看到了完整的路径：“结合形式化，我看到了一种可以利用AI系统化推进数学研究的方法。”他在数学中心公众号上发了一条推文《AI for Mathematics：数学智能副驾驶的构想》，讲他的判断。“很多人觉得我异想天开。”

这不是他第一次在没有路标的方向上押注。2016年他还没拿到北大长聘教职就转入深度学习研究，在当时同样不被看好。他说自己“胆子大”，习惯选“大多数人觉得不可能的事情”来做——“做不出来，反正大多数人都说不可能。做出来，一定让大家大吃一惊。”

刘若川是一位做数论研究的基础数学家，他看出来AI辅助数学研究的出现对基础数学来说是一场根本性的变革：“如果别人要革我的命，那我还不如自己革自己的命。”他并不确定AI究竟能走多远，但他确定一件事：不能站在原地看着变化发生。

肖梁也是数论领域的基础数学家。他对AI没有董彬那样激进的预期，但他觉得值得参与。“对我们来讲这是一个长期的投资，参与这个项目很开心，接触到最新的AI和数学结合的东西。”他更想做的是结合人的思考，把AI的能力用起来。

文再文的加入最有戏剧性。2023年初，他每天中午吃完饭跟董彬他们围着镜春园和朗润园的湖泊遛弯，“就被‘安利’说GPT多厉害”。他让两位本科生试了一道优化题，发现能做，就这样慢慢开始了。他的主要研究领域是优化，也做AI算法，在数学和AI两边都有积累，在团队中自然承担起了连接两边的角色。

四个人，四种理由，在北大的日常碰撞中走到了一起。没有外部项目牵引，没有行政指令。“2023年那会儿你去做AI for Math，没有什么具体项目可以申。老师们还是凭兴趣。”董彬是这么认为的。

2023年，团队正式组建。学生陆续加入，本硕博全都有，还有外来交流人员。背景差异大：计算机、AI、纯数、应用数学都有。有同学大一就加入了团队。“真正坚定跟着我们干的学生，早期可能就那么几个，大家也都会有怀疑。”没有人许诺过什么确定的未来。一群人，各自的理由，走向了同一个方向。

打地基

方向定了，但什么都没有。没有数据库，没有检索工具，没有形式化基础设施。连Lean形式化方法，团队也是从零学起。通过数学中心同事訚琪峥请来了他的师弟、Lean技术专家约汉·科姆林（Johan Commelin）在线授课，后来肖梁还邀请到了帝国理工学院的凯文·巴扎德（Kevin Buzzard）来北大参加工作坊，他是推动数学家使用Lean的标志性人物。学会的同学再教下一批同学，一层一层传下去。团队还在多所兄弟院校开设LEAN培训课程。有学生认为，相关培训对国内Lean形式化学习和推广起到了带动作用。

数学家做研究，第一步是查文献、找定理。在Lean数学库中检索已形式化的内容，往往要耗费大量时间。团队开发了LeanSearch，用自然语言描述即可语义检索Lean 4数学库中的相关定理。上线后，LeanSearch被纳入Lean官方工具，截至2026年5月底累计调用已逾800万次。

自然语言文献的检索同样重要。团队开发了Matlas，覆盖上千万条数学陈述，支持语义检索，能定位到跨子领域的相关结论。LeanSearch覆盖形式化世界，Matlas覆盖自然语言世界，两个引擎组合起来，检索能力覆盖了数学研究的两侧。

文再文带队推进了大量“基础设施”建设。M2F系统将自然语言证明转化为形式化语言，利用Lean逐步检查每一个推理步骤是否成立。团队构建了形式化数学库ReasBook，收录超过27万行Lean代码。他做的工具分两部分：“一部分面向数学本身，帮助数学家做计算、做证明、整理文档；另一部分面向更广的群体，让数学和应用触手可及。”文再文跟团队还搭建了ReasLab在线平台，约1000名用户无需安装即可使用形式化工具，降低了数学家的工具使用门槛。

“我们做的工具，首先要自己愿意用，否则就没有任何意义。”董彬说。

这些是别人看不见的苦功。“总得有人做这些事。学生们自己也清楚，基础设施不搭好，后面什么都做不了，所以大家一起扛了很长时间非常工程的活儿。现在慢慢开始收获了。”学生们的日常不是推导定理，而是“这5个按钮怎么还没做”。小而精的团队，要有选择地投入。“我们的选择就是用最强的AI模型，把我们对数学的理解注入到AI系统中去攻克最难的问题。”

这些基础设施的搭建需要持续投入。早期团队在AI4Math领域籍籍无名，又正是需要资源的时候。能够心无旁骛地投入一个前景未明的方向，离不开稳定的支持。董彬、刘若川、肖梁先后获得新基石科学基金支持。北大数学院友姚齐聪在关键阶段给予支持，他作为联创创立的九坤量化助力团队渡过资源最紧张时期。此后，九坤发起成立至知创新研究院（IQuest Research），在北大 AI4MATH 项目的数据标注、处理与模型训练等方面持续协作，提供了有力支持。

目前北大AI4MATH团队正参与相关国际社区建设，主导研发的部分工具被形式化数学社区用户使用。数学形式化研究是一个需要下苦功夫的长期性工程，北大数学正在做拓荒工作，研究进展以开源方式发布，并面向国内相关团队开展交流。他们的工作正惠及整个中国数学研究社区。

LeanSearch检索工具界面

系统架构示意图

让AI上场

2024年，外部节奏突然加快。谷歌AI团队的多个数学系统接连取得进展，然后AlphaProof这一数学系统出来了。

“发现跟我们的技术路径一模一样，但是他们工程远远领先于我们。”这是对团队打击最大的时刻。每次DeepMind这一机构发布新工作，团队都得立刻集中讨论，看看对自己意味着什么，下一步怎么走。

但董彬依然从紧迫的形势中看到了北大数学团队的优势，“方向不一样。企业做和数学相关的工作，更多是展示能力。但对我们来说，数学就是我们的全部。”

团队以北大数学本科习题集中的100道证明题为样本测试模型能力，发现在自然语言层面，模型的证明能力已经达到较高水平。到2025年初，模型在北大数学博士资格考试水平的测试集上取得了80分以上的平均分。董彬觉得，可以开始让AI尝试解决数学猜想了。

肖梁负责选题。“就像带博士生一样，你不能上来就给他黎曼猜想。要先给他一个难度适中的问题，让他了解证明的过程，熟悉领域和方法。训练AI也是这个道理。”安德森猜想（Anderson猜想，代数几何与表示论领域的重要问题）是他选定的目标之一。该猜想由美国数学家安德森（D.D. Anderson，主要从事交换代数领域研究）于2014年提出（Problem 8a），追问交换代数中拟完备局部环的两个弱化层级是否等价，提出十余年来一直悬而未决。

Rethlas-Archon联合系统开始工作。Rethlas负责探索：搜索文献、提出猜测、尝试构造、遇到矛盾后回溯调整，在多轮试错中逼近可行的证明路径。Archon负责形式化验证：将自然语言证明翻译成Lean 4代码（一种形式化证明语言）并验证其正确性，相当于为证明落下法槌。

关键发现出现在检索环节。Rethlas通过Matlas语义检索，从上千万条数学陈述中发现了拟完备性理论与Jensen（2006）的形式纤维（formal fiber）构造之间的跨域联系。这种联系横跨两个不同的数学子领域，人类通常需要两位不同方向的专家碰面才可能建立。Rethlas据此构造反例，否定了Anderson猜想。

随后Archon基于团队此前构建的M2F形式化系统，将证明转化为近两万行Lean 4代码。这个过程不是简单的翻译：Archon在验证中自主发现了初始方案的逻辑漏洞，推翻了原来的路线，重新设计了证明路径。它还需要把六篇不同论文中的核心结论串联起来，拼成一条完整的逻辑链。相关代码和证明仍待社区进一步检验。

虽然“做出来了”，但这个领域的发展是真正的日新月异，进展非常快。中国要在AI4MATH这个全新的前沿领域占得一席之地，必须全速奔跑。团队的学生与老师们一同面对着外部竞争的压力，“领域发展快，同行出东西快，我们就在组会上仔细拆解分析，看看能不能做改进。”

Rethlas的能力并不止于交换代数。近期，北大数学科学学院刘济豪基于 Rethlas搭建了能力更强的专用智能体，通过数学家与 AI 系统的深度协作，解决了代数几何领域多个公开问题。这表明 Rethlas的"跨域搭桥"能力具有通用性，也展示了有经验的数学家与 AI 系统深度结合后能释放出的巨大研究潜能。

这是一个属于年轻人的领域。除了领头的几位教授外，刘若川的学生姜杰东（现在西湖大学做博士后研究），以及还在北大读博士的居浩成、高国雄、陈乐恒、王梓琛、王语同、何婉仪等学生辈，正成长为团队的中坚力量。

Rethlas-Archon智能体协作流程示意图

Anderson猜想的形式化证明代码

这群人在想什么

AI正在改变数学研究的可能性边界。这条路到底能走多远，没有人知道。

一个有意思的张力持续存在于团队内部。有的成员想尽可能多地形式化已有数学，有的想让流程更自动化，让数学家用起来越来越轻松。同时，大家都希望保持数学家的主体地位。这种张力没有被消解，也不需要消解。

肖梁的看法是：“AI会带来一种新的思考数学问题的范式。它擅长从海量现象里提取信息，人也可以，但信息太复杂的时候AI更好。”他同时保留着一个判断：“最精妙的数学还需要人的直觉，目前AI做不了那种‘天上掉下来’的感觉。”

董彬的回应是：“AI是一个能力的放大器，能帮我们解决更大的问题。”他在意的不是AI能否替代数学家，而是AI和数学之间更深层的关系。“当有一天我们不再说‘AI+数学’，说明这件事做成了。就像我们从来不说‘LaTeX+’，因为那是必备技能。”

董彬说：“我们做这个事情的出发点就是数学本身。”企业的AI团队相对更关注模型总体性能指标，而这里关心的是数学能不能被真正推进。

这种差异体现在具体的技术选择中。团队构建的每一层基础设施，数学认知都在起作用。选择去构建检索引擎，是因为团队知道数学研究中找到不同陈述和证明之间的内在关联、搭起桥梁是至关重要的。而构建Rethlas、Archon、M2F这类智能体，需要熟悉数学家的工作方式和思维模式，知道他们在每一步会怎么想、会卡在哪里。这些东西，只有既懂数学又关心数学发展的人才做得出来。

刘若川（左上）董斌（右上）文再文（左下）肖梁（右下）

开源是团队从一开始就坚持的立场。Rethlas、Archon、LeanSearch均已开源，技术报告和形式化代码全部公开。团队公开了用Archon做形式化验证的实际成本，比此前很多人预想的要便宜很多。“公开成本数据很重要，这有助于让更多团队参与进来。”董彬说。

团队的氛围从学生那里能感受到。“老师很有包容性，不同想法都愿意听。”不管是教授还是学生，“头脑风暴的时候，大家都差不多”，谁有想法谁说。组会每周四两次，早上一次晚上一次。微信群里大家经常交流讨论最新的研究进展，“这也是一个放松的时间”。

这种氛围不是凭空产生的。

刘若川讲过他对科研生态的理解：“做科学最重要的一点是宽松的环境。你不能什么都上纲上线、可丁可卯，什么都计划好。科学研究总是伴随着不确定性，突破往往源于意外，不能完全预设。”他用了一个比喻：“最重要的是有一个好的生态——有湿地、湖泊、平原、山坡，生物在里面自然繁衍。”

“做好数学这件事，说到底就是把最好的人引进来，给他们自由发挥的空间。你不能期盼他一定会做出什么，但大批优秀的人在一起，总会做出好东西。”

“如果说有什么困难的话，那可能还是国内做这方面工作的人还是太少了，我们希望有越来越多人能参与到这项事业中。”

在无尽的未知中

刘若川对AI辅助数学研究的前景表示乐观，并且认为进展可能比大多数人预期的更快，但他也有担忧。AI提供的是具体的实践知识（know-how），如果人连这一层知识都依赖机器，能力会分化：少部分人底层能力扎实，用AI放大后会很强；但如果基本功没打好就依赖AI，差距反而会拉大。

文再文对此有类似的判断：“数学的教育模式肯定会有大变化，但一些基本训练是慢的过程，需要时间沉淀。比如数分要学一年半，这是基本能力的训练。读博士是一个漫长的过程，需要跨过很多道坎。这些东西不是轻易能被替代的。”

刘若川在去年当选为中国科学院院士，并于今年年初接任北京大学数学科学学院院长。角色变了，肩负的责任也随之而变，他需要更多考虑新形势下的学科发展和人才培养。除了AI4MATH（AI辅助数学研究），同样重要的是MATH4AI（数学反哺人工智能研究），“数学是人工智能的逻辑基石，除了要持续投入数学形式化与AI辅助数学研究，加快构建数学研究新范式外，还要同时考虑反哺大模型数学推理能力提升。”现在，他经常在周一下午大步流星地赶回怀新园，参加团队的讨论班，与同事们和同学们一起学习新知，思考未来。“未来需要的是复合型人才，数学功底扎实，同时懂AI、有跨学科的视野。数学训练给人的抽象和推理能力的价值在AI时代不是在减弱，而是在增强。但只有这些不够，新一代数学人还需要学会与AI协作，学会跨越学科的边界。”

董彬对这个问题的回答带着数学家的气质：“数学是一种让我们必须诚实面对自己的语言。我希望未来，这种语言不再只是少数人的小语种，而能够成为更多人理解世界的工具。”

这条路走到今天，回头看，团队做对了一些事，也走过弯路，前面依然看不清。有学生在采访中说：“还处在早期阶段，艰难探索。”这句话没有修饰，但也许最接近真实。路很长，不确定的东西远比确定的多，但他们选择继续往前走。