Chapters
In reading order. The Lean half builds the tools; the causal-inference half spends them. Each chapter names the files under lean/ its code comes from, and every one of those is compiled in CI.
Lean
The language and its proof assistant, from a background of statistics rather than type theory.
- 00WelcomeWhat this tutorial assumes, what it does not, and a first look at every kind of thing a chapter can contain.
- 01Terms, types, propositionsA statement is a type, a proof is a term, and checking a proof is type-checking. Functions, definitions, and the six connectives, with the smallest examples that make each one clear.
- 02TacticsThe goal state as the object of attention: every tactic you need, one worked example each, how to read an error message, and how to make Lean find the Mathlib lemma for you.
- 03Reals and finite sumsℝ, coercions, division by zero, Fin n, Finset, and the sum lemmas that carry every proof in Part II. The mean is linear, deviations sum to zero, and the variance identity.
- 04Structures and definitionsBundling data with `structure`, controlling how a definition unfolds, extensionality, summing over all 2^n assignments — and the finite-population library rebuilt in miniature.
- 05Mathlib and autoformalizationHow Mathlib is organized and named, how to read a statement you did not write, and a checklist for auditing an autoformalized theorem before you believe it.
Causal inference
Finite-population, design-based inference: potential outcomes, randomization, unbiasedness, variance.
- 06Potential outcomesThe finite-population model as the library defines it: two outcome vectors, assignments as treated sets, the real-valued indicator, the observed outcome — and the fundamental problem of causal inference as a theorem.
- 07DesignsThe assignment mechanism as an explicit probability mass function: expectation as a finite sum, propensities, and the two designs everything later is built on.
- 08UnbiasednessHorvitz–Thompson is unbiased under any design with strictly interior propensities; difference in means is unbiased under complete randomization.
- 09VarianceNeyman's variance formula for difference in means, and why the variance estimator everyone reports is conservative.
- 10Blocking and clusteringThe pushforward of a design; stratified randomization and why difference in means breaks; the blocked estimator; cluster randomization for free.
- 11Regression as linear algebraIn a finite population an OLS coefficient is an algebraic identity about the observed data. The coefficient on a treatment dummy is the difference in means, group dummies return group means, and the fully interacted regression is two within-group fits.
- 12Fisher randomization testsThe sharp null, exact imputation, and a p-value that is a finite sum over the design; validity as a counting argument, with the hypothesis the informal statement forgets.
- 13Partial identificationManski worst-case bounds in a finite population: the identified set is exactly a closed interval, its width is the range of the outcome, and randomization does not shrink it.
- 14Bridge to Mathlib's probabilityThe finite-sum tutorial translated into measure theory: pmfs, ℝ≥0∞, integrals, independence — and how to read an autoformalized probability statement.
Appendix
Reference material, tactic cheat-sheets and the verification pipeline.
- A1Tactic cheatsheetEvery tactic taught in this tutorial, one row each, grouped by what it does to the goal, plus the error messages you will actually hit.
- A2GlossaryA Lean-to-statistics dictionary, plus every definition and theorem this library exports, one line each with a link to where it is introduced.
- A3How this site is verifiedThe pipeline behind the claim that every Lean result on this site is machine-checked, and how to reproduce every step of it yourself.