Lean 4 for Program Verification in the Age of AI

Leonardo de Moura — Marktoberdorf Summer School, Herrsching am Ammersee, August 2026

  1. Introduction to Lean and Dependent Type Theory
  2. Programming and Proving in Lean
  3. Proof Automation and AI
  4. Software Verification in Lean