Reading Theorems in Lean

Overview

As formalization tools like Lean 4 become increasingly capable, the mathematical community faces a new challenge: while a machine can perfectly verify a proof, ensuring that a formal statement accurately reflects the intended mathematical theorem remains an irreducibly human task. This seminar offers an introduction to Lean designed specifically around reading and understanding formal definitions and theorem statements rather than writing proof scripts. We will explore the overarching goals of auto-formalization, focusing on creating auditable bridges between machine-checked code and ordinary mathematical prose. Furthermore, we will discuss why researchers should care about this translation process. By examining recent formalization efforts, we will demonstrate how translating mathematics into Lean systematically surfaces implicit assumptions, enforces rigorous boundary conditions, and exposes tacit regularity gaps that often go unnoticed in traditional peer review. Ultimately, the seminar will highlight how formalization acts not just as a verification tool, but as a mechanism to clarify mathematical communication and enable domain experts to audit statements without needing to be Lean experts themselves.