2. Mathematics
This part opens with the foundations — the everyday vocabulary (propositions, proofs, and sets), the universes and axioms on which Lean's mathematics rests, and well-foundedness and the avoidance of paradoxes — and then surveys parts of Mathlib that go beyond first-year mathematics: order theory and lattices, the algebraic hierarchy, filters as a unifying language for limits, topology and measure theory, and discrete probability. The aim is not to redo the mathematics from scratch but to show how Mathlib organizes it — which typeclasses to use, where to find the lemmas, and what the design trade-offs were.
Each chapter starts with a short notation table so the symbols are
introduced before they appear, and uses Verso's {docstring} block
to render Mathlib definitions and lemmas inline so the notes stay in
sync with the library.
2.1. Sets and Types
This section is published right before the chapter is taught.
2.1.1. Sets versus types
This section is published right before the chapter is taught.
2.1.2. Notation and naming conventions
This section is published right before the chapter is taught.
2.1.3. Sets are predicates
This section is published right before the chapter is taught.
2.1.4. Subset, union, intersection, complement
This section is published right before the chapter is taught.
2.1.5. Indexed unions and intersections
This section is published right before the chapter is taught.
2.1.6. Set equality
This section is published right before the chapter is taught.
2.1.7. From a set back to a type: subtypes and coercion
This section is published right before the chapter is taught.
2.2. Universes, Axioms, and Foundations
This section is published right before the chapter is taught.
2.2.1. Prop vs Type: proof irrelevance
This section is published right before the chapter is taught.
2.2.2. The Calculus of Inductive Constructions
This section is published right before the chapter is taught.
2.2.3. The axioms of Lean
This section is published right before the chapter is taught.
Propositional extensionality (propext)
This section is published right before the chapter is taught.
The axiom of quotients
This section is published right before the chapter is taught.
The axiom of choice (Classical.choice)
This section is published right before the chapter is taught.
2.2.4. What is not an axiom: funext and excluded middle
This section is published right before the chapter is taught.
Function extensionality is a theorem
This section is published right before the chapter is taught.
Excluded middle is a theorem (Diaconescu)
This section is published right before the chapter is taught.
2.2.5. Declared axioms vs. what the kernel bakes in
This section is published right before the chapter is taught.
More that the kernel bakes in
This section is published right before the chapter is taught.
What this means
This section is published right before the chapter is taught.
2.2.6. Why the kernel has no loops
This section is published right before the chapter is taught.
Recursors instead of recursion
This section is published right before the chapter is taught.
The second door: strict positivity
This section is published right before the chapter is taught.
Non-termination is allowed, just not in proofs
This section is published right before the chapter is taught.
2.2.7. Constructive vs classical logic
This section is published right before the chapter is taught.
Excluded middle in use
This section is published right before the chapter is taught.
Decidability, classically
This section is published right before the chapter is taught.
When do you need Classical.choice?
This section is published right before the chapter is taught.
2.2.8. Comparison with ZFC set theory
This section is published right before the chapter is taught.
2.2.9. Brief mention of other type theories
This section is published right before the chapter is taught.
2.3. Well-Foundedness and Paradoxes
This section is published right before the chapter is taught.
2.3.1. Accessibility and well-founded relations
This section is published right before the chapter is taught.
2.3.2. Why Nat is well-founded
This section is published right before the chapter is taught.
2.3.3. Why s ∈ s is impossible
This section is published right before the chapter is taught.
2.3.4. Two kinds of "no vicious circle"
This section is published right before the chapter is taught.
2.4. Orders, Lattices, and Complete Lattices
This section is published right before the chapter is taught.
2.4.1. Notation and naming conventions
This section is published right before the chapter is taught.
2.4.2. Partial orders
This section is published right before the chapter is taught.
2.4.3. The power set as a partial order
This section is published right before the chapter is taught.
2.4.4. Lattices
This section is published right before the chapter is taught.
2.4.5. Complete lattices
This section is published right before the chapter is taught.
2.4.6. Monotone and antitone functions
This section is published right before the chapter is taught.
2.4.7. The Knaster-Tarski fixed point theorem
This section is published right before the chapter is taught.
2.4.8. Summary of key API
This section is published right before the chapter is taught.
2.4.9. Exercises
This section is published right before the chapter is taught.
2.5. The Algebraic Hierarchy in Mathlib
This section is published right before the chapter is taught.
2.5.1. Notation and naming conventions
This section is published right before the chapter is taught.
2.5.2. From operations to monoids
This section is published right before the chapter is taught.
2.5.3. Groups
This section is published right before the chapter is taught.
2.5.4. Rings and fields
This section is published right before the chapter is taught.
2.5.5. Morphisms
This section is published right before the chapter is taught.
2.5.6. Substructures
This section is published right before the chapter is taught.
2.5.7. Quotient structures
This section is published right before the chapter is taught.
2.5.8. The ext tactic for algebraic structures
This section is published right before the chapter is taught.
2.5.9. Navigating the hierarchy
This section is published right before the chapter is taught.
2.6. Filters in Mathlib
This section is published right before the chapter is taught.
2.6.1. Notation and naming conventions
This section is published right before the chapter is taught.
2.6.2. Motivation: why filters?
This section is published right before the chapter is taught.
2.6.3. Filters as generalized subsets
This section is published right before the chapter is taught.
2.6.4. The formal definition
This section is published right before the chapter is taught.
2.6.5. The order on filters
This section is published right before the chapter is taught.
2.6.6. The principal filter
This section is published right before the chapter is taught.
2.6.7. The atTop filter
This section is published right before the chapter is taught.
2.6.8. The cofinite filter
This section is published right before the chapter is taught.
2.6.9. Filter.map: the pushforward
This section is published right before the chapter is taught.
2.6.10. Filter.Tendsto: the general notion of limit
This section is published right before the chapter is taught.
2.6.11. Filter.Eventually and Filter.Frequently
This section is published right before the chapter is taught.
2.6.12. A worked example: 1 / (n + 1) → 0
This section is published right before the chapter is taught.
2.6.13. Ultrafilters
This section is published right before the chapter is taught.
2.6.14. Why filters are better for formalization
This section is published right before the chapter is taught.
2.7. Topology via Filters
This section is published right before the chapter is taught.
2.7.1. Notation and naming conventions
This section is published right before the chapter is taught.
2.7.2. TopologicalSpace
This section is published right before the chapter is taught.
2.7.3. Open and closed sets
This section is published right before the chapter is taught.
2.7.4. Closure, interior, and frontier
This section is published right before the chapter is taught.
2.7.5. The neighborhood filter nhds
This section is published right before the chapter is taught.
2.7.6. Continuity via Tendsto
This section is published right before the chapter is taught.
2.7.7. Compact spaces
This section is published right before the chapter is taught.
2.7.8. Connected spaces
This section is published right before the chapter is taught.
2.7.9. Metric spaces
This section is published right before the chapter is taught.
2.7.10. Continuity in metric spaces
This section is published right before the chapter is taught.
2.7.11. Product topology
This section is published right before the chapter is taught.
2.7.12. Summary of key Mathlib API for topology
This section is published right before the chapter is taught.
2.8. Measure Theory in Mathlib
This section is published right before the chapter is taught.
2.8.1. Notation and naming conventions
This section is published right before the chapter is taught.
2.8.2. Sigma-algebras: MeasurableSpace
This section is published right before the chapter is taught.
2.8.3. Measurable functions
This section is published right before the chapter is taught.
2.8.4. Measures
This section is published right before the chapter is taught.
2.8.5. The Lebesgue measure on ℝ
This section is published right before the chapter is taught.
2.8.6. A small worked computation
This section is published right before the chapter is taught.
2.8.7. Integration
This section is published right before the chapter is taught.
2.8.8. Convergence theorems
This section is published right before the chapter is taught.
2.8.9. Probability measures
This section is published right before the chapter is taught.
2.8.10. Almost everywhere and ae-filter
This section is published right before the chapter is taught.
2.8.11. Conditional expectation
This section is published right before the chapter is taught.
2.8.12. Summary of key Mathlib API for measure theory
This section is published right before the chapter is taught.
2.9. Monads and Probability Mass Functions
This section is published right before the chapter is taught.
2.9.1. Monads: the general pattern
This section is published right before the chapter is taught.
The problem: chaining computations that may fail
This section is published right before the chapter is taught.
The Bind operation
This section is published right before the chapter is taught.
The do-notation
This section is published right before the chapter is taught.
The Functor typeclass
This section is published right before the chapter is taught.
The Monad typeclass
This section is published right before the chapter is taught.
Lists as a monad
This section is published right before the chapter is taught.
The IO monad
This section is published right before the chapter is taught.
Stateful computation with StateM
This section is published right before the chapter is taught.
Error handling with Except
This section is published right before the chapter is taught.
Sets as a monad
This section is published right before the chapter is taught.
Filters as a monad
This section is published right before the chapter is taught.
Finite sets and Finset
This section is published right before the chapter is taught.
Connection to category theory
This section is published right before the chapter is taught.
Summary of monads seen so far
This section is published right before the chapter is taught.
2.9.2. Probability mass functions
This section is published right before the chapter is taught.
Notation and naming conventions
This section is published right before the chapter is taught.
The definition
This section is published right before the chapter is taught.
pure: the Dirac distribution
This section is published right before the chapter is taught.
bind: composing distributions
This section is published right before the chapter is taught.
map: pushing a distribution along a function
This section is published right before the chapter is taught.
join: flattening distributions of distributions
This section is published right before the chapter is taught.
The Monad PMF instance
This section is published right before the chapter is taught.
Concrete distributions
This section is published right before the chapter is taught.
Beyond PMFs: measures, expectation, independence
This section is published right before the chapter is taught.
When do we still need measurability?
This section is published right before the chapter is taught.