始作“勇”者：一群北大数学教授的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 Journal上。
Peking Mathematical Journal 论文截图
这是团队第一次主动用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检索工具界面
系统架构示意图
2024年，外部节奏突然加快。谷歌AI团队的多个数学系统接连取得进展，然后AlphaProof这一数学系统出来了。
“发现跟我们的技术路径一模一样，但是他们工程远远领先于我们。”这是对团队打击最大的时刻。每次DeepMind这一机构发布新工作，团队都得立刻集中讨论，看看对自己意味着什么，下一步怎么走。
但董彬依然从紧迫的形势中看到了北大数学团队的优势，“方向不一样。企业做和数学相关的工作，更多是展示能力。但对我们来说，数学就是我们的全部。”
团队以北大数学本科习题集中的100道证明题为样本测试模型能力，发现在自然语言层面，模型的证明能力已经达到较高水平。到2025年初，模型在北大数学博士资格考试水平的测试集上取得了80分以上的平均分。董彬觉得，可以开始让AI尝试解决数学猜想了。
肖梁负责选题。“就像带博士生一样，你不能上来就给他黎曼猜想。要先给他一个难度适中的问题，让他了解证明的过程，熟悉领域和方法。训练AI也是这个道理。”安德森猜想（Anderson猜想，代数几何与表示论领域的重要问题）是他选定的目标之一。该猜想由美国数学家安德森（D.D. Anderson，主要从事交换代数领域研究）于2014年提出（Problem 8a），追问交换代数中拟完备局部环的两个弱化层级是否等价，提出十余年来一直悬而未决。
