Formalizing mathematics using proof assistants enables eliminating errors, encourages collaborative mathematics, and can lead to deeper understanding. This graduate course provides an introduction to using Lean proof assistant to formalize mathematical definitions and theorems. We will give an overview of foundations of formal proof and dependent type theory of Lean. We will also explore how to leverage proof tactics (such as simp, rw, ring, linarith) to automate up proof construction. In addition, we will explore how AI assistants based on large language models can make the formalization process more productive. Finally, in the second half of the course we will work on a formalization project (to be chosen in class) together.
- Professor: Thomas Bourgeat
- Professor: Friedrich Eisenbrand
- Professor: Viktor Kuncak
- Professor: Ola Nils Anders Svensson
- Professor: Maryna Viazovska
- Professor: Thomas Vidick
- Teacher: Jonathan Conrad
