The Development of Lean and the Type Theoretic Foundation of Theorem Provers
Time: 2024-01-29
Published By: Xiaoni Tan
Speaker(s): Minchao Wu (University of Tokyo)
Time: 16:00-17:00 January 30, 2024
Venue: Online
腾讯会议：304-163-177
内容：在这个讨论班中我将介绍Lean的发展与定理证明器的类型论基础。以 “AI for Mathematics：数学形式化和定理证明” 2023年寒假培训班同学感兴趣的话题为脉络，探讨类型论作为元理论与数学证明及其自动化的关联；以及Lean作为一个形式化数学的环境，是如何与机器学习，尤其是近期风靡的大语言模型结合，从而实现一定程度上优于基于传统逻辑方法的自动化的。
BIO： 吴敏超，现在在东京大学计算机系博士后。研究方向是 formal verification 及其自动化。硕士期间在 CMU 做交互式定理证明的研究，导师是 Jeremy Avigad，也由此了解了早期的 Lean。博士期间在澳大利亚国立大学师从 Michael Norrish，从事对定理证明器 HOL4 自动化的研究。
