“AI for Mathematics：数学形式化和定理证明” 2025年寒假培训班报名通知
近年来，人工智能赋能科学研究的”AI for Science”新范式蓬勃发展，然而人工智能在数学领域，特别是在定理证明方面仍充满挑战。传统上数学形式化和定理证明由数学家完成，但是这种方式需要花费大量时间和精力，并且存在人为疏漏和错误的风险。人工智能的发展给数学形式化和定理证明带来了新的机遇，比如Deepmind AlphaProof在测试2024国际数学奥林匹克竞赛题时可以达到银牌水平。
东莞市大湾区高等研究院智能计算研究中心将于2025年1月13日-1月19日开设数学形式化培训班，在全国范围内招收不超过30名优秀本科生。培训班旨在探索利用人工智能技术推动数学形式化和定理证明的发展，进一步提高定理证明的效率和准确性，帮助验证一些相关领域中关键定理证明。
培训班在北京大学文再文教授的指导下学习和推进数学优化方面的形式化证明。欢迎学有余力并对研究工作有兴趣的本科生报名参加！
一、报名条件：
1、学习成绩优秀、学有余力的本科生。
a)课程要求：数学分析、高等代数、泛函分析、数值分析、数值代数、最优化等基础课程成绩优秀。
b)具备一定编程基础，如能熟练运用Python编程，能够快速学习新的编程工具。
2、写作/阅读能力：中英文写作能力强，能熟练阅读英文文献
3、有充裕的时间和精力投入，积极参与交流讨论，听从导师与助教的安排和指导。
二、报名材料
1、本科阶段成绩单（学校教务部门出具）1份
2、报名表
下载附件：《报名表》
三、基本考评要求
完成Lean提供的mathematics_in_lean中课后练习题
四、报名方式
1、网上报名：点击网址：https://www.wjx.cn/vm/O6y8gGk.aspx# ，填写在线报名表。
2、 将成绩单和签字盖章的报名表按照以上顺序合并转成一个PDF文档，发送至邮箱：cinco@gbu.edu.cn，邮件主题命名格式为：学生姓名+学校名称。
（注：以邮件收到的成绩单等报名材料为准，仅在网上报名而不按照要求发送电子材料视为报名无效。）
3、报名截止日期为2024年12月23日。录取结果将于2024年12月30日前通过邮件通知。
4、本次课程无须缴纳学费，为非本地学员提供住宿（2人合住），为非本校学生提供培训期间用餐，交通等其他费用自理。
五、培训地点
大湾区大学（筹）松山湖校区（广东省东莞市松山湖大学路16号）
六、联系方式
联系人：易老师
Email：cinco@gbu.edu.cn
