Time: 19:00-20:00, Wednesday, May 7 2025
Venue：E4-233
Speaker: Paul-André Melliès, Université Paris Cité
Biography: 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.
Title：Exploring the logic of mathematical proof assistants
Abstract: 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.
