Lean 4 for design-based causal inference
Proofs you can run, about designs you already trust
A tutorial in Lean 4 for people who arrive already fluent in probability, estimators and experimental design, and entirely new to a proof assistant. Instead of the usual march through type theory, it formalizes the thing you already know cold: finite-population, design-based causal inference — potential outcomes, complete randomization, unbiasedness, the variance of the difference in means.
Every chapter is a mix of prose, informal statements set beside their Lean forms, and exercises you finish in the browser, with hints and solutions. Every proof shown is machine-checked. You do not install anything.
Contents
Lean
The language and its proof assistant, from a background of statistics rather than type theory.
- 00WelcomeAn introduction to Lean 4 through design-based causal inference, with instructions for running the examples.
- 01Terms, types, propositionsTerms, types, propositions, functions, definitions, and the logical connectives used in Lean statements.
- 02TacticsGoal states, common proof tactics, error messages, and tools for finding Mathlib lemmas.
- 03Reals and finite sumsReal numbers, coercions, division, finite index types, finite sums, means, and variance identities.
- 04Structures and definitionsStructures, definitions, extensionality, and a compact finite-population model.
- 05Mathlib and autoformalizationMathlib organization and search, followed by a checklist for auditing autoformalized statements.
Causal inference
Finite-population, design-based inference: potential outcomes, randomization, unbiasedness, variance.
- 06Potential outcomesPotential outcomes, treatment assignments, observed outcomes, and non-identification in a finite population.
- 07DesignsAssignment mechanisms as probability mass functions, with expectations, propensities, and standard designs.
- 08UnbiasednessHorvitz–Thompson is unbiased under any design with strictly interior propensities; difference in means is unbiased under complete randomization.
- 09VarianceNeyman's exact variance formula for difference in means and the conservativeness of its usual estimator.
- 10Blocking and clusteringPushforward designs, stratified randomization, blocked estimators, and cluster randomization.
- 11Regression as linear algebraOLS as linear algebra: treatment indicators, group means, and fully interacted regressions.
- 12Fisher randomization testsSharp null hypotheses, exact imputation, randomization p-values, and finite-sample validity.
- 13Partial identificationManski worst-case bounds, sharpness, and identified sets in a finite population.
- 14Bridge to Mathlib's probabilityTranslating finite designs into Mathlib probability: pmfs, measures, integrals, and independence.
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 verifiedWhat "machine-checked" means for the proofs on these pages, and how to check them yourself.