时间: 2025年8月22日（周五）13:30-17:30
地点: E10-205
主讲人: Patrick Massot, Université Paris-Saclay
主讲人介绍：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.
讲座主题: Why explain mathematics to computers?
讲座摘要: 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.
