2025年上海交通大学数学科学学院“AI4Math：Lean4与数学形式化”暑期学校报名通知

保研资讯小站长

近年来，大语言模型的推理能力，尤其是在数学问题求解和证明中的应用成为一大研究热点。然而，数学对推理的严谨性要求极高，单纯依赖语言模型极易出现幻觉等错误。如何将数学的知识与逻辑融入大语言模型，以消除幻觉、提升推理能力和保证严谨性受到日益增加的关注。过去几年，数学形式化逐渐成为一个被广泛采用的可行途径。目前，数学形式化的主要工具为Lean4等，该语言功能强大，但入门门槛较高，限制了它的普及度。

基于上述背景，上海交通大学数学科学学院机器学习研究所、自然科学研究院，北京大学国际数学研究中心和国际机器学习研究中心拟联合举办“AI4Math：Lean4与数学形式化”暑期学校，以推广Lean4语言和数学形式化，推动AI4Math的发展。本次暑期学校将包含两个专题，分别为专题一：Lean4基础和专题二：数值代数形式化。

组织者：

罗涛，上海交通大学数学科学学院副教授

梁经纬，上海交通大学自然科学研究院副教授

董彬，北京大学国际数学研究中心教授

文再文，北京大学国际数学研究中心教授

专题一： Lean4基础

时间：2025年7月14 - 20日

规模：计划招生人数为25人。

一、报名条件

1.数学或计算机科学等相关专业的本科生或低年级研究生。

2.具有较强的数学素养，对数学形式化感兴趣。

3.具备一定编程基础的学生优先考虑。

二、食宿安排

为非上海地区的学生提供住宿补助1000元，为所有同学提供餐费补助300元。

三、课程安排

完成分组课题，并进行展示。在学员的意愿基础上，择优选择部分学生进入专题二继续学习。

专题二：数值代数与形式化

时间：2025年7月14日 - 2025年8月3日

规模：招生人数为20人。

一、报名条件

1.数学或计算机科学等相关专业的二三年级本科生优先考虑。

2.有编程基础、数值代数相关基础的学生优先考虑。

3.有数学或相关竞赛经历的学生优先考虑。

4.结课后仍能持续投入时间和精力：积极参与交流讨论，听从导师与助教的安排和指导。

二、食宿安排

为非上海地区的同学提供免费住宿，为所有同学提供餐费补助300元/周。

三、课程安排

1.第一阶段（7月14-20日）：进行Lean4的学习，完成Lean提供的Mathematics in Lean中10道练习题。

2.第二阶段：

a.（7月21-27日）协助整理数学定理证明的自然言语版本；完成导师指定的数值代数相关的形式化证明。

b.（7月28日-8月3日）进行数值代数的形式化。

3.第三阶段：我们将从完成第二阶段的学员中择优选择10名同学，于8月底集中进行数学形式化工作。具体细节将另行通知。

注：前两周都设有考核，不达标的同学不能继续下一阶段的学习。

报名材料与方式

一、报名材料

1.成绩单（教务部门出具）。

2.竞赛获奖证书等补充材料。

3.个人简历和陈述。

二、报名方式

1.网上报名：

通过网址https://wj.sjtu.edu.cn/q/bKSvNqG5填写在线报名表。（注：交大学生也要报名）

2.将报名材料按照报名材料顺序合并转成一个PDF文档，文档命名格式为：“专题一/二+学生姓名+学校名称”（如专题一+张三+上海交通大学）。将电子文档发送至邮箱：AI4MathSJTU@163.com，邮件主题命名格式为：`专题一/二+学生姓名+学校名称`。

注：以邮件收到的报名材料为准，仅在网上报名而不按照要求发送电子材料视为报名无效。

3.报名截止日期为2025年6月15日。

结业形式

1.两个专题的学生完成相应的课程任务后可获得结业证书。

2.表现优异的学生将获得组委会颁发的荣誉证书。

联系方式

邮箱：AI4MathSJTU@163.com

课程大纲

课程时间：2025年7月14日 - 2025年8月3日

专题一： 2025年7月14日 - 2025年7月20日

专题二： 2025年7月14日 - 2025年8月3日

数值代数授课老师：罗涛，梁经纬

参考资料：

1.Lean4安装上手指南:

http://faculty.bicmr.pku.edu.cn/~wenzw/formal/docs/#/zh-cn/

2.Matrixcookbook:

https://www.math.uwaterloo.ca/~hwolkowi/matrixcookbook.pdf

3.Mathematics in Lean:

https://leanprover-community.github.io/mathematics_in_lean/

4.Metaprogramming in Lean:

https://leanprover-community.github.io/lean4-metaprogramming-book/

5.Theorem proving in Lean4: 

https://leanprover.github.io/theorem_proving_in_lean4/

6.ReasLab: https://alpha.reaslab.io/