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