MrCLean

Chapters

In reading order. The Lean half builds the tools; the causal-inference half spends them.

Lean

The language and its proof assistant, from a background of statistics rather than type theory.

  1. 00WelcomeAn introduction to Lean 4 through design-based causal inference, with instructions for running the examples.
  2. 01Terms, types, propositionsTerms, types, propositions, functions, definitions, and the logical connectives used in Lean statements.
  3. 02TacticsGoal states, common proof tactics, error messages, and tools for finding Mathlib lemmas.
  4. 03Reals and finite sumsReal numbers, coercions, division, finite index types, finite sums, means, and variance identities.
  5. 04Structures and definitionsStructures, definitions, extensionality, and a compact finite-population model.
  6. 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.

  1. 06Potential outcomesPotential outcomes, treatment assignments, observed outcomes, and non-identification in a finite population.
  2. 07DesignsAssignment mechanisms as probability mass functions, with expectations, propensities, and standard designs.
  3. 08UnbiasednessHorvitz–Thompson is unbiased under any design with strictly interior propensities; difference in means is unbiased under complete randomization.
  4. 09VarianceNeyman's exact variance formula for difference in means and the conservativeness of its usual estimator.
  5. 10Blocking and clusteringPushforward designs, stratified randomization, blocked estimators, and cluster randomization.
  6. 11Regression as linear algebraOLS as linear algebra: treatment indicators, group means, and fully interacted regressions.
  7. 12Fisher randomization testsSharp null hypotheses, exact imputation, randomization p-values, and finite-sample validity.
  8. 13Partial identificationManski worst-case bounds, sharpness, and identified sets in a finite population.
  9. 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.

  1. 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.
  2. A2GlossaryA Lean-to-statistics dictionary, plus every definition and theorem this library exports, one line each with a link to where it is introduced.
  3. A3How this site is verifiedWhat "machine-checked" means for the proofs on these pages, and how to check them yourself.