四川大学“AI4Math：Lean4与数学形式化”
寒假培训班报名通知
近年来，大语言模型的推理能力，尤其是在数学问题求解和证明中的应用成为一大研究热点。然而，数学对推理的严谨性要求极高，单纯依赖语言模型极易出现幻觉等错误。如何将数学的知识与逻辑融入大语言模型，以消除幻觉、提升推理能力和保证严谨性受到日益增加的关注。过去几年，数学形式化逐渐成为一个被广泛采用的可行途径。目前，数学形式化的主要工具为Lean4等，该语言功能强大，但入门门槛较高，限制了它的普及度。
基于上述背景，国家天元数学西南中心、四川大学数学学院，北京大学北京国际数学研究中心拟联合举办“AI4Math：Lean4与数学形式化” 寒假培训班，以推广Lean4语言和数学形式化，推动AI4Math的发展。
组织
王治国，四川大学数学学院副教授
连增，四川大学数学学院教授
文再文，北京大学北京国际数学研究中心教授
专题： Lean4基础培训
时间：2026年1月19日 - 1月30日。
规模：计划招生人数为30人。
（一）报名条件
1. 学习成绩优秀、学有余力的本科生。
a) 课程要求：数学分析、高等代数、泛函分析、数值分析、数值代数、最优化等基础课程成绩优秀。
b) 具备一定编程基础，如能熟练运用Python编程，能够快速学习新的编程工具。
2. 写作/阅读能力：中英文写作能力强，能熟练阅读英文文献。
3. 有充裕的时间和精力投入，积极参与交流讨论，听从导师与助教的安排和指导。
4. 具有较强的数学素养，对数学形式化感兴趣。
（二）食宿安排
为非成都地区的学生免费提供住宿，为所有同学提供餐费补助300元/每周。
（三）课程安排
1. 第一阶段（1月19日 - 1月25日）
l 进行整数规划的学习，协助整理数学定理证明的自然言语版本。
l 进行Lean4的学习，完成Lean提供的Mathematics in Lean中10道练习题。
整数规划部分授课教师：徐芦泽 助理教授
专家简介：徐芦泽博士目前是威斯康星大学麦迪逊分校的博士后研究员。他将于 2026 年 1 月加入香港科技大学（HKUST）数学系，担任助理教授。他的研究兴趣包括全局优化、整数规划、混合整数规划，以及联系连续优化与离散优化的相关理论。在威斯康星大学麦迪逊分校任现职之前，他曾是加州大学戴维斯分校数学系的 Krener 助理教授。他于 2022 年获得密歇根大学工业与运筹工程博士学位，并于 2017 年获得北京大学计算数学学士学位。徐芦泽博士曾荣获多个奖项，包括 INFORMS优化协会青年学者奖（2024年）。
2. 第二阶段：（1月26日 - 1月30日）
l 协助整理完善数学定理证明的自然言语版本；完成导师指定的整数规划相关的形式化证明。
l 进行整数规划理论和算法的形式化。
（四）报名材料与方式
一、报名材料
1.成绩单（教务部门出具）
2.竞赛获奖证书等补充材料。
3.个人简历和陈述。
二、报名方式
1.网上报名：
https://tianyuan.scu.edu.cn/portal/activities/registration/id/2/p/210.html
2.将报名材料按照报名材料顺序合并转成一个PDF文档，文档命名格式为：“Lean4基础+学生姓名+学校名称”（如Lean4基础+张三+四川大学）。将电子文档发送至邮箱：tianyuan_southwest@163.com，邮件主题命名格式为：“Lean4基础+学生姓名+学校名称”。
注：以邮件收到的报名材料为准，仅在网上报名而不按照要求发送电子材料视为报名无效。
3.报名截止日期为2025年12月19日。
培训班将在后台对报名人员信息进行审核，并根据报名情况，对学员名额进行调整。
（五）结业形式
1.所有学生完成相应的课程任务后可获得结业证书。
2.表现优异的学生将获得组委会颁发的荣誉证书。
（六）联系方式
邓老师 邮箱：yibodeng@scu.edu.cn
刘老师 邮箱：sw_center_liuzj@163.com
一、课程大纲
第一阶段：1月19日 – 1月25日
第二阶段：1月26日 - 1月30日
参考资料：
1. Lean在线协同编辑ReasLab IDE:
2. Mathematics in Lean:
https://leanprover-community.github.io/mathematics_in_lean/
3. Metaprogramming in Lean:
https://leanprover-community.github.io/lean4-metaprogramming-book/
4. Theorem proving in Lean4:
https://leanprover.github.io/theorem_proving_in_lean4/