时间：2025年5月7日（星期三）19:00-20:00
地点：E4-233
主讲人: Paul-André Melliès, Université Paris Cité
主讲人简介: Paul-André Melliès is a CNRS Senior Researcher member of the Laboratoire IRIF at the Department of Computer Science of the Université Paris Cité. He is also a member of the INRIA Picube team. His research interests include Mathematical logic, proof theory, game semantics, theory and practice of programming languages, computer architecture, formalized mathematics, proof assistants, mathematical physics, knot theory, quantum groups, n-dimensional algebra, operads.
讲座主题：Exploring the logic of mathematical proof assistants
讲座摘要: In this introductory talk, I will describe the logical foundations of interactive theorem provers such as Lean or Rocq, and give some basic examples of how these proof assistants work on simple concrete mathematical problems. I will also explain how ongoing research at the intersection of homotopy type theory, game semantics, and natural language processing is providing new perspectives on the design and implementation of these proof assistants.
