近年来，人工智能赋能科学研究的“AI for Science”新范式蓬勃发展，然而人工智能在数学领域，特别是在定理证明方面仍充满挑战。传统上数学形式化和定理证明由数学家完成，但是这种方式需要花费大量时间和精力，并且存在人为疏漏和错误的风险。人工智能的发展给数学形式化和定理证明带来了新的机遇，比如Deepmind AlphaProof在测试2024国际数学奥林匹克竞赛题时可以达到银牌水平。

在此背景下，武汉大学将开设数学形式化短课程，旨在探索利用人工智能技术推动数学形式化和定理证明的发展，进一步提高定理证明的效率和准确性，帮助验证一些相关领域中关键定理证明。短课程将在北京大学文再文教授的指导下学习和推进数学优化方面的形式化证明。欢迎学有余力并对研究工作有兴趣的同学报名参加！

一、课程说明

课程日期：2024年11月27日-12月01日

课程时间：上午9:30-11:30，下午14:30-16:30，其余时间上机练习

授课地点：武汉大学校内（具体地点见录取通知）

主办单位：国家天元数学中部中心、武汉大学数学与统计学院、武汉数学与智能研究院、湖北国家应用数学中心

二、组织委员会

张平文、杨志坚、文再文、焦雨领等

三、招生对象

1、全国范围内学习成绩优秀、学有余力的本科生。（名额不超过30人）

（1）课程要求：数学分析、高等代数、泛函分析、数值分析、数值代数、微分方程、微分方程数值解等基础课程成绩优秀。

（2）具备一定编程基础，如能熟练运用Python编程，能够快速学习新的编程工具。

2、写作/阅读能力：中英文写作能力强，能熟练阅读英文文献。

3、有充裕的时间和精力投入，积极参与交流讨论，听从导师与助教的安排和指导。

四、基本考评要求

完成Lean提供的mathematics_in_lean中10道练习题。

五、报名及录取

1、 报名方式与材料：

（1）点击网址提交报名信息（https://jsj.top/f/TOoQYr），或扫描下方二维码提交报名信息：

（2）外校学生提交报名信息后，请至国家天元数学中部中心官方网站报名通知页面底部下载《附表:天元中部中心短课程报名表》（https://tmcc.whu.edu.cn/info/1051/14991.htm），填写签字盖章后扫描为PDF文档，文档命名格式为：学生姓名+学校名称。将电子文档发送至指定邮箱（tmcc@whu.edu.cn），邮件主题命名格式为：学生姓名+学校名称。武汉大学在校学生无需填写此表。

（注：外校学员仅在网上报名而不按照要求发送电子材料视为报名无效。）

2、报名截止日期：2024年11月14日。我们将邮件通知每一位通过报名的学员。

3、本次短课程无须缴纳学费，为非本地学员提供住宿（2人合住），为非本校学生提供餐补，费用由国家天元数学中部中心承担，交通等其他费用自理。

六、联系方式

李老师；电话：027-87287715；

邮箱：tmcc@whu.edu.cn