Welcome

This chapter is a placeholder: it exists so that every piece of machinery the real chapters rely on is exercised at least once. Read it as a tour of the furniture rather than as a lesson.¹The tutorial proper begins with the next chapter. If you are reading this on the deployed site and the next chapter does not exist yet, that is why.

What you are assumed to know

You know what an estimator is, you are comfortable with $\mathbb{E}[\cdot ]$ and $\mathrm{Var}(\cdot )$, and you have written down the difference-in-means estimator

more than once. You are assumed to know nothing at all about type theory, dependent types, tactics, or why anyone would want a proof assistant.

What a chapter contains

Prose and ordinary code

Most Lean in a chapter is illustration, and appears as a plain fenced block. It is highlighted but not runnable, which is the right default:

-- A `Finset` is a finite set with a decidable membership test.
-- Design-based inference lives almost entirely in this type.
example : (Finset.range 3).card = 3 := by simp

Statements, informal beside formal

The recurring move of the tutorial is to put an English claim next to the Lean proposition that is supposed to mean the same thing, and then argue about whether it does.

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

Runnable blocks

A <LeanBlock> is a code block you can execute. The preamble — here just import Mathlib — is hidden on the page but travels with the code to the playground, so what you run always type-checks.

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

Snippets lifted from the verified sources

The block above has its Lean written inline, which is fine for a two-line example. Anything load-bearing is instead quoted out of a file that CI compiles. <Snippet> names the file and the region:

/-- The very first thing anyone proves. `decide` evaluates both sides. -/
theorem two_plus_two : (2 : ℕ) + 2 = 4 := by
  decide

If that region were renamed or deleted, this page would fail to build rather than silently going stale.

Exercises

An exercise is the same machinery with the proof removed. The posed version has a sorry where the answer goes; the answer is one <details> away and is itself runnable.

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

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 same exercise, generated from the -- SOLUTION markers in the verified source rather than written out twice:

/-- The average of a constant over a non-empty index set is that constant.

This is the smallest statement in the tutorial that already needs `0 < n`: at
`n = 0` the sum is `0` and the division is `0 / 0 = 0`, which happens to be
`c` only when `c = 0`. -/
theorem mean_const (n : ℕ) (hn : 0 < n) (c : ℝ) :
    (∑ _i ∈ Finset.range n, c) / n = c := by
  sorry

/-- The average of a constant over a non-empty index set is that constant.

This is the smallest statement in the tutorial that already needs `0 < n`: at
`n = 0` the sum is `0` and the division is `0 / 0 = 0`, which happens to be
`c` only when `c = 0`. -/
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

Where to go next

Chapter numbering is by reading order, not by file name, so chapters can be inserted without renumbering URLs. Use the previous/next links at the foot of each chapter, or the chapter list.