Formal Mathematics for Mathematicians and Mathematics Students - IPAM at UCLA

Explore the potential impact of formal mathematics on mathematical exposition in this 55-minute conference talk by Patrick Massot from Université Paris-Saclay. Delve into how formal methods can benefit mathematicians beyond proof verification, with a focus on their application in teaching and communicating mathematical concepts. Witness a demonstration of readable proof scripts, English translations, and the use of AI tools in formalizing mathematical proofs. Gain insights into topics such as general topology, proof structure, and the future of formal mathematics in academic settings. Discover practical examples using Lean, a theorem prover and programming language, and learn how it can be applied to complex mathematical concepts like open sets, neighborhoods, and subsets.

Intro
Topology
General topology
Proof structure
Formalization
readable proof script
English translation
Open AI DaVinci
Tiny URL
Gold State
Close Neighborhood
Set Image Subset
Lean Informal
Future steps
Complicated proof
Unreliable proof
Technical talk
Lean code
Simp
Proof in Lean
Python
Lean