Lecture slides

One reveal.js deck per lecture — to follow the talk live. ← back to the course

1. A general introduction to type theoryopen →
2. Simple calculations with the Church λ-calculusopen →
3. Propositional logic proofsopen →
4. Introduction to Leanopen →
5. Advanced Leanopen →
6. Auto-formalization of mathematics with Leanopen →

The full notes are in the knowledge book and the interactive material in the Lambda Lab.