About
A tutorial that teaches Lean 4 by formalizing the causal inference its reader already knows.
Introductions to proof assistants tend to be written for people who want a proof assistant. This one is written for a statistician or an ML researcher who wants something else: a way to know that an argument about an estimator is actually airtight, including the boring parts — the index sets, the edge case at n = 0, the place where an expectation quietly changed measure — and a way to read the formal statements they are increasingly handed by other people and by machines.
Design-based causal inference is the vehicle because it is finite, combinatorial and free of measure-theoretic overhead: the randomization is a draw from a finite set of assignment vectors, so the probability is counting, and the Lean can be about the substance from the first chapter.
Every proof on these pages is machine-checked. The Lean lives in the repository, compiled against Mathlib, and the chapters quote it rather than retyping it; anything genuinely unproved is written sorry and says so. The runnable blocks hand their code to the community Lean web editor at https://live.lean-lang.org, so nothing needs installing.
Written by Drew Dimmery. Corrections and questions are welcome as issues on the repository.