Mini Course on Type Theory and Lean

类型论与自动定理证明 迷你课程

徐天一

• 第一讲：3月14日14:25 - 17:05，邯郸校区H6502
• 第二讲：3月15日9:55 - 12:30，邯郸校区HGX202
  前两讲直播：腾讯会议：911-7170-3944，密码：666666
  课件、录像
• 答疑与实操辅导：3月16日9:55 - 12:30，邯郸校区HGW2403
• 第 $n$ 讲（$n\geq 2$）：待定

课程简介

在计算机科学与数学的交汇处，类型论不仅是现代编程语言与形式化验证的基石，更为自动定理证明提供了强大的理论工具。本短期课程将讨论类型论的核心思想及其在自动定理证明中的应用，兼顾理论与实践，为了解相关领域打下基础。

课程亮点

基础与前沿结合：从简单类型 λ-演算出发，逐步讨论依值类型、同伦类型论等进阶主题，揭示类型系统如何严谨表达数学命题。
工具实践导向：通过 Lean 4 证明系统实践，学习将数学证明编码为可验证的代码的方法，掌握形式化验证的关键技术。
与 AI 结合：探讨将传统自动证明技术与生成式人工智能结合的可能方案，提供 AI for math 入门讲解。

讲师简介

徐天一本科毕业于复旦大学数学科学学院，硕士毕业于新加坡国立大学数学系。现就职于北京国际数学研究中心 Al for math 课题组，负责 Lean 4 相关工具的开发及数据增强算法的设计与实现。

主办单位：复旦大学哲学学院