Interactive Theorem Proving using Lean, Winter 2026/27

 Interactive Theorem Proving using Lean, Winter 2026/27🔗

Peter Pfaffelhuber

Notes for a course on formal proving with the interactive theorem prover Lean 4 (below simply Lean), winter semester 2026/27, University of Freiburg. Start with the Introduction; hardware, installation and the run of the semester are at its end.

Contents

  1. Introduction
  2. 1. Lean and its type theory
  3. 2. Mathematics
  4. 3. Appendix
  5. 4. Projects
  6. 5. Bibliography
  7. 6. Slides