Stefano M. Nicoletti

Reasoning, Proof, and Formalization with Lean 4

A Gentle Introduction to Lean for Beginners

Lecture notes, Lean classroom files, exercises, and solutions.

Upcoming lectures

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 materials