Reasoning, Proof, and Formalization with Lean 4
A Gentle Introduction to Lean for Beginners
Lecture notes, Lean classroom files, exercises, and solutions.
Upcoming lectures
- Monday, 19 October 2026, 16:00–17:30
Lecture materials
Lecture 1Lecture 1: What Is an Interactive Theorem Prover?Open materialsLecture 2Lecture 2: Propositions, Proofs, and Logical RulesOpen materialsLecture 3Lecture 3: From Natural Deduction to Proofs in LeanOpen materialsLecture 4Lecture 4: Classical Logic and QuantifiersOpen materialsLecture 5Lecture 5: Quantifier RulesOpen materialsLecture 6Lecture 6: Inductive Types, Recursion, and InductionOpen materialsLecture 7Lecture 7: Induction, Simplification, and Software VerificationOpen materials