Welcome — MrCLean

This book introduces Lean 4 to readers who know statistics but not formal proof. It develops the language through design-based causal inference, beginning with the difference-in-means estimator and the assumptions used to study it.

Why use a proof assistant

Informal proofs routinely omit algebraic steps and boundary cases. A proof assistant requires each assumption to be stated and each step to be justified. For example, a theorem about difference in means must specify that both treatment groups are nonempty; otherwise division by zero remains part of the statement.

Lean checks that a proof establishes its formal statement from the stated definitions and assumptions. It cannot check that the statement matches the intended informal claim. This distinction is especially important for generated formalizations, where a valid proof may accompany a weak, vacuous, or mis-specified theorem. Each chapter therefore includes examples of statements that compile but fail to express the advertised result.

Why design-based causal inference

The finite-population, design-based view of an experiment fixes the units, fixes their potential outcomes, and lets one thing be random: which units get treated. The experimenter chose the mechanism that makes it random. So an expectation is a weighted sum over the $2^{n}$ possible treated sets, a variance is another one, and unbiasedness of an estimator is an identity between two finite sums.

This setting is well suited to an introductory formalization. Expectations and variances can be defined by finite sums, so the early chapters require no measure theory or integrability conditions. Chapter 14 connects these finite definitions to Mathlib’s general probability library.

Prerequisites

The book assumes familiarity with estimators, expectations, variances, and the difference-in-means estimator

\hat{τ} = \frac{1}{n_{1}} \sum_{i : Z_{i} = 1} Y_{i} - \frac{1}{n_{0}} \sum_{i : Z_{i} = 0} Y_{i}

No background in type theory, dependent types, tactics, or proof assistants is required.

Informal beside formal

The chapters place informal claims beside their proposed Lean statements and compare them explicitly. The first example is:

TheoremMean of a constant

The average of a constant $c$ over $n$ units is $c$ .

Note what the English left out and the Lean did not: the hypothesis 0 < n, that is, $n \geq 1$ . Without it the sum is $0$ , the division is $0 / 0 = 0$ in Lean’s convention, and the statement is false for every $c \neq 0$ .

New tab

theorem mean_const (n : ℕ) (hn : 0 < n) (c : ℝ) :
    (∑ _i ∈ Finset.range n, c) / n = c := by
  rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
  have : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn.ne'
  field_simp

In the formal statement, (∑ _i ∈ Finset.range n, c) / n is the sum of $n$ copies of $c$ divided by $n$ ; (hn : 0 < n) is a hypothesis the theorem may use; and := by introduces the proof. Chapters 1–3 explain this notation, and Chapter 4 develops similar definitions.

Running the Lean

Every executable Lean block has two controls in its top-right corner. Check it (or Run in playground, or Try in playground) opens the Lean web editor directly below the block, with the code loaded; New tab opens the same thing in its own tab. The first load has to start a Lean server with Mathlib and takes a few seconds. Errors and the current goal appear in the panel to the right of the code, or below it on a narrow screen. No local installation is required.

Your first proofNew tab

theorem two_plus_two : (2 : ℕ) + 2 = 4 := by
  decide

Running the block and changing 4 to 5 demonstrates that decide rejects a false proposition.

Some blocks note that they open with a long preamble. The later chapters build on a library of definitions, and the editor has to see those definitions before it can check the code on the page, so they travel along, above it. Scroll to the bottom of the editor for the code you were reading.

Exercises

An exercise contains sorry in place of a proof. Lean accepts sorry but emits a warning, so the task is to replace it with a complete proof. Exercises are classified as warm-up, core, or stretch and include a hint and a runnable solution.

ExerciseMean of a constant

Prove the statement from above: the average of a constant $c$ over $n \geq 1$ units is $c$ .

New tab

theorem mean_const (n : ℕ) (hn : 0 < n) (c : ℝ) :
    (∑ _i ∈ Finset.range n, c) / n = c := by
  sorry

Hint

Finset.sum_const turns the sum into n • c and Finset.card_range makes the n explicit; nsmul_eq_mul turns • into *. The goal is then ↑n * c / ↑n = c, and field_simp will close it once it knows (n : ℝ) ≠ 0, which is Nat.cast_ne_zero.mpr hn.ne'.

Show solution

New tab

theorem mean_const (n : ℕ) (hn : 0 < n) (c : ℝ) :
    (∑ _i ∈ Finset.range n, c) / n = c := by
  rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
  have : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn.ne'
  field_simp

The route

Part I (chapters 1 to 5) teaches enough Lean to read and write the statements this tutorial cares about: terms and types, tactics, real numbers and finite sums, structures, and how to find your way around Mathlib. Part II (chapters 6 to 14) is the causal inference: potential outcomes, designs, unbiasedness, variance, blocking and clustering, regression, randomization tests, partial identification, and finally the bridge to Mathlib’s probability theory. Two appendices — a tactic cheat sheet and a glossary — are for looking things up.

Chapters are meant to be read in order, with the exercises. Use the previous/next links at the foot of each chapter, or the chapter list.