6. Slides🔗

Some chapters have a deck, used in the lecture and readable on its own. The figures and claims are those of the text, so either can be used without the other.

• Why formalize? -- the first lecture: what formalizing means, where things stand in 2026, the four episodes and the landmark formalizations.

• Filters in Mathlib -- accompanies the chapter on filters.

Press s in a deck for the speaker notes, o for an overview of all slides, and ? for the remaining keys. Every slide carries a link in its upper right corner that leads back to this page.