A talk from the Formal Methods in Mathematics workshop in Pittsburgh, January 2020: Speaker: Patrick Massot
Title: Formalizing a Sophisticated Definition
Slides:
Abstract:
In this talk I'll try to explain what it means to formalize a sophisticated definition, using mostly the example of perfectoid spaces that I formalized in Lean with Kevin Buzzard and Johan Commelin. Then I will show examples where the peculiarities of type theory and formal proofs initially looked like a nuisance to us, but actually led us to improve a mathematical story. I will not assume familiarity with perfectoid spaces or any other mathematical topic beyond the basics of general topology.
0 Comments