3. Projects
The exercise sheets cover the first half of the semester. The second half is devoted to individual projects: pick a topic, formalize it in Lean, present the result. Five suggestions follow, each with a description, a sketch of one implementation and references. A first working version of any of them fits into a few hundred lines, and each has stretch goals beyond that.
You are equally welcome to propose a topic of your own — for example, formalizing an exercise from your first year of studies, or exploring a corner of Mathlib that interests you — as long as you discuss the scope with us first.
3.1. Project 1: Girard's paradox, or why Type : Type is fatal
This section is published right before the chapter is taught.
3.2. Project 2: Cantor-Schröder-Bernstein via Knaster-Tarski
This section is published right before the chapter is taught.
3.3. Project 3: Limits of sequences, with and without filters
This section is published right before the chapter is taught.
3.4. Project 4: The integers from scratch
This section is published right before the chapter is taught.
3.5. Project 5: The Monty Hall problem with the PMF monad
This section is published right before the chapter is taught.