Time: 14:00-15:00, Friday, August 22 2025
Venue: E10-205
Speaker: Patrick Massot, Université Paris-Saclay
Biography：Patrick Massot works as a professor at the Laboratoire de Mathématiques d'Orsay in Université Paris-Saclay. His research focuses on contact geometry and symplectic geometry. Recently he worked a lot on formalized mathematics. In particular he formalized the definition of perfectoid spaces with Buzzard and Commelin. He's contributed to the Liquid tensor experiment. He also formalized sphere eversions.
Title: Why explain mathematics to computers?
Abstract: In this talk I'll explain what it means to "explain mathematics to a computer" and why I find it interesting and useful. I'll show what it's like to use software to encode definitions, statements and proofs. I'll present applications of these techniques to verify, explain, teach or create mathematics. I'll mention examples of non-trivial projects in this field and briefly mention links with AI. There are no prerequisites.
