AI 辅助数学科研和教学的一点实践分享

报告人：马家骏（厦门大学）

时  间：2026年8月31日10:00

地  点：海韵园实验楼S103 & 腾讯会议ID: 897-528-319

内容摘要:

近一年，AI 和形式化工具在数学中的进展来得很快。若干前沿 AI 系统已经达到国际数学奥林匹克金牌水平，也开始参与发现、证明甚至证伪一些有深度的数学猜想；另一方面，在 AI 系统的辅助下，Lean 形式化也在明显加速，从强素数定理的快速形式化，到高维球堆积问题的机器验证，都显示出形式化数学正在进入一个新的阶段。

本报告谈谈自己在这方面的一些尝试。报告主要包括三个方面。首先，介绍如何在论文写作过程中同步推进形式化验证，以及如何借助 AI 编程做计算实验、探索例子和验证数学猜想。其次，讨论数学分支领域形式化基础库的建设：从 Computational Economics 形式化库，到Lie 理论、表示论和 Langlands 纲领形式化库，探讨不同数学分支如何逐步建立自己的形式化基础设施。最后，分享 AI 在教学中的一些使用经验。

通过这些具体例子，我想说明的是，AI 与形式化工具并不只属于“AI 证明困难猜想”这样的宏大叙事。它们也可以很具体、很日常地进入普通数学工作者的学习、研究和教学。

个人简介：

马家骏，厦门大学数学科学学院副教授。2013年获新加坡国立大学博士学位，先后在新加坡国立大学、香港中文大学数学科学研究所、以色列 Ben-Gurion 大学从事博士后研究，2017至2021年任上海交通大学副教授。研究方向为约化群表示论、Theta 对应与局部 Langlands 纲领。

联系人：周达