
2026年6月18日上午,首场北大数学AI for Math使用交流会在北京国际数学研究中心甲乙丙楼报告厅举行。活动旨在介绍北京大学在人工智能赋能数学研究方面的最新进展,探讨AI技术如何支持数学发现、证明验证、科研协作和应用建模。数学中心创始主任田刚院士、副主任张继平院士,中国科学技术协会副主席袁亚湘院士,中国数学会副理事长、广州南方学院校长汤涛院士,中山大学香港高等研究院首席科学家张益唐教授,北京大学数学科学学院党委书记胡俊教授等出席活动,来自北京大学和周边高校、科研院所的百余位师生参加活动并参与讨论。活动由数学科学学院院长刘若川院士和数学中心张磊教授联合主持。
活动正式开始前,田刚院士、汤涛院士、袁亚湘院士先后致辞。他们表示,北大数学人才辈出,勇于攻坚克难,北大数学在AI for MATH这一新兴领域在较短时间内取得前沿研究成果和建设成效,令人欣喜。AI for MATH正在成为数学研究的重要前沿方向,他们期待北大青年学者把握人工智能发展机遇,在数学与人工智能交叉领域持续探索、形成更多具有影响力的成果,带动中国数学在AI时代取得更大发展。

田刚院士致辞

汤涛院士致辞

袁亚湘院士致辞


刘若川院士、张磊教授联合主持活动
接下来,董彬教授首先以“人工智能赋能数学研究—智能体设计与实践”为题作报告。他指出,人工智能正在改变数学研究的范式,但数学文献跨域关联难以发现、自然语言证明与形式化验证之间鸿沟巨大等瓶颈依然突出。他随后介绍了北京大学课题组构建的三个数学研究智能体:基于Lean 4自动生成和验证数学证明的形式化验证智能体Archon、基于大规模数学检索的推理智能体Rethlas、以及面向计算数学、支持数值算法自动推导与验证Iteris,重点展示了这些智能体的设计思路和在解决数学开放问题中的典型案例。在报告最后,董彬对AI驱动的数学研究未来方向作简要展望。

董彬报告
随后,文再文以“ReasLab:智能数学推理引擎展示”为题作报告。他围绕ReasLab的建设理念、系统架构和核心能力,介绍了其作为AI for Math时代数学研究基础设施的探索。ReasLab面向数学教育、数学研究与应用建模场景,融合大语言模型、多智能体协作、数学模型库、算法库、定理库与云端工作空间,支持问题理解、数学建模、计算求解、形式化验证、代码执行和报告写作等环节的贯通协同。作为云端平台,用户无需本地安装,即可在线开展优化建模、Lean形式化、科研写作与协作。目前,ReasLab 已为上千位用户提供支持,并在高校教学科研和企业应用场景中开展使用。报告后,文再文课题组对ReasLab的主要功能模块进行了现场操作演示。

文再文报告
会议还设置了功能演示区,吸引了不少与会人员上手体验并交流使用场景。

参会师生在功能演示区试用、交流
在问答交流环节,与会师生围绕人工智能时代数学研究的基础价值、数学智能体的发展路径、科研论文的学术意义以及智能数学推理平台建设等问题进行了深入交流。针对AI发展是否会削弱基础数学研究价值、青年学者如何应对新变化等问题,董彬指出,人工智能为数学研究提供了新的工具体系,但数学研究仍需不断拓展理论边界,青年学者应主动借助AI工具提升研究能力,在问题理解、理论判断和跨学科协作中形成自身核心竞争力。围绕数学智能体能否从基础规则出发实现自主探索,董彬进一步表示,这一方向具有重要前沿意义,但数学研究复杂度极高,仍需要长期深入探索。
围绕ReasLab平台建设和AI辅助论文写作等问题,文再文指出,智能数学推理平台的核心在于面向数学教育、科研和应用建模场景,构建开放、可适配、可协同的研究环境。随着基础模型能力不断提升,平台应能够灵活接入不同模型和工具,将建模、计算、验证、写作与协作等环节有机贯通。他同时表示,AI可以提升写作、建模、编程和验证效率,但论文的核心价值并不只是文字表达,而在于问题提出、方法构建、逻辑论证、结果验证和同行交流;研究者对问题价值、理论意义和结论可靠性的判断仍不可替代。
张益唐教授结合解析数论研究谈到,许多数学问题本身也包含探索和实验的成分,需要不断寻找合适对象和有效方法,人工智能有望在这类探索性研究中发挥新的辅助作用。

张益唐教授在交流环节发言




活动现场
目前,由董彬、刘若川、文再文、肖梁等青年教师领衔的北大AI for MATH团队正参与相关国际社区建设,主导研发的部分工具被形式化数学社区用户使用,研究进展以开源方式发布,并面向国内相关团队开展交流。此次交流会中介绍的这些工具在真实数学研究场景中持续迭代,每一轮与数学家的协作都在推动工具能力的边界向前移动。正是数学研究者的实际需求在直接牵引工具的演进方向。此次活动的主要目的之一便是促进中国数学界,特别是年轻一代在相关领域内的共识和行动,共同推动智能时代数学研究新范式的发展。正如田刚院士在总结陈词中指出的,“在人工智能快速发展的新时代,数学家仍将继续发挥重要作用,希望青年学者把握机遇、勇于创新,持续推进数学与人工智能的深度融合。”
Rethlas、Archon、Iteris开源仓库:
https://github.com/frenzymath/Rethlas
https://github.com/frenzymath/Archon
https://github.com/frenzymath/iteris
blog: https://frenzymath.com/
ReasLab及智能体:
https://model.reaslab.io
ReasBook开源仓库:
https://github.com/optpku/ReasBook
blog: https://blog.reaslab.io/
北大科研
科研成果|前沿动态|科研沙龙
长按扫码关注我们

来源: 北京大学北京国际数学研究中心
夜雨聆风