已发布！上海交通大学“AI4Math：Lean4与数学形式化”暑期学校，下面小编简单介绍下此次夏令营申请条件、申请办法及时间、申请材料等重要信息内容。
近年来，大语言模型的推理能力，尤其是在数学问题求解和证明中的应用成为一大研究热点。然而，数学对推理的严谨性要求极高，单纯依赖语言模型极易出现幻觉等错误。如何将数学的知识与逻辑融入大语言模型，以消除幻觉、提升推理能力和保证严谨性受到日益增加的关注。过去几年，数学形式化逐渐成为一个被广泛采用的可行途径。目前，数学形式化的主要工具为Lean4等，该语言功能强大，但入门门槛较高，限制了它的普及度。
基于上述背景，上海交通大学数学科学学院机器学习研究所、自然科学研究院，北京大学国际数学研究中心和国际机器学习研究中心拟联合举办“AI4Math：Lean4与数学形式化”暑期学校，以推广Lean4语言和数学形式化，推动AI4Math的发展。本次暑期学校将包含两个专题，分别为专题一：Lean4基础和专题二：数值代数形式化。
组织者：
罗涛，上海交通大学数学科学学院副教授
梁经纬，上海交通大学自然科学研究院副教授
董彬，北京大学国际数学研究中心教授
文再文，北京大学国际数学研究中心教授
专题一：Lean4基础
时间：2025年7月14日-20日
规模：计划招生人数为25人
一、报名条件：
数学或计算机科学等相关专业的本科生或低年级研究生
具有较强的数学素养，对数学形式化感兴趣
具备一定编程基础的学生优先考虑
二、食宿安排：
为非上海地区的学生提供住宿补助1000元，为所有同学提供餐费补助300元。
三、考核方式：
完成分组课题，并进行展示。在学员的意愿基础上，择优选择部分学生进入专题二继续学习。
专题二：数值代数与形式化
时间：2025年7月14日-2025年8月3日
规模：招生人数为20人
一、报名条件：
数学或计算机科学等相关专业的二三年级本科生优先考虑。
有编程基础、数值代数相关基础的学生优先考虑。
有数学或相关竞赛经历的学生优先考虑。
结课后仍能持续投入时间和精力：积极参与交流讨论，听从导师与助教的安排和指导。
二、食宿安排：
为非上海地区的同学提供免费住宿，为所有同学提供餐费补助300元/周。
三、课程安排：
第一阶段：（7月14日-20日）进行Lean4的学习，完成Lean提供的Mathematics in Lean中10道练习题。
第二阶段：（7月21日-27日）协助整理数学定理证明的自然言语版本；完成导师指定的数值代数相关的形式化证明。
（7月28日-8月3日）进行数值代数的形式化。
第三阶段：我们将从完成第二阶段的学员中择优选择10名同学，于8月底集中进行数学形式化工作。具体细节将另行通知。
注：前两周都设有考核，不达标的同学不能继续下一阶段的学习。
报名材料与方式:
一、报名材料：
成绩单（教务部门出具）
竞赛获奖证书等补充材料
个人简历和陈述
二、报名方式：
网上报名：点击网址：https://wj.sjtu.edu.cn/q/bKSvNqG5，填写在线报名表。（注：交大学生也要报名）
将报名材料按照报名材料顺序合并转成一个PDF文档，文档命名格式为：“专题一/二+学生姓名+学校名称”（如专题一+张三+上海交通大学）。将电子文档发送至邮箱：AI4MathSJTU 163.com，邮件主题命名格式为：”专题一/二+学生姓名+学校名称“。注：以邮件收到的报名材料为准，仅在网上报名而不按照要求发送电子材料视为报名无效。
报名截止日期为2025年6月15日。
结业形式:
两个专题的学生完成相应的课程任务后可获得结业证书。
表现优异的学生将获得组委会颁发的荣誉证书。
联系方式:
邮箱：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/
注：以上内容仅供参考，详细信息请联系在线辅导老师了解。
以上就是【上海交通大学“AI4Math：Lean4与数学形式化”暑期学校，保研人速看！】的全部内容了。如果大家还想了解更多内容，可登录高顿保研频道或者咨询右下角在线辅导老师。
