Formal Mathematics with Lean and AI

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 proof construction. In addition, we will explore whether 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. Forms of instruction will include: Lectures Hands-on tutorials Feedback on homeworks Grading will be based on Participation Homeworks Developing and presenting formalized Lean proofs Content: Overview of formal axiomatic approaches; first-order logic, set theory, classical higher-order logic Dependent Type Theory and Calculus of Constructions Inductive Definitions Tactics in Lean Lean as a programming language Mathlib4 design Collaborative formal mathematics using Lean blueprints Autoformalization using LLM agents