Mathlib and autoformalization

Reading generated or unfamiliar Lean requires two skills. First, the reader must identify Mathlib definitions and locate the lemmas that govern them. Second, the reader must check that a formal statement expresses the intended mathematical claim. Compilation establishes that the proof has the stated type; it does not establish that the statement is an adequate formalization.

The first half of this chapter introduces Mathlib’s naming and search tools. The second gives a checklist for detecting statements that are vacuous, too weak, over-specialized, or based on unintended definitions. The flawed examples are designed to compile so that the error must be found in the statement.

Part one: reading Mathlib

Mathlib is a single library — well over a million lines of Lean — covering most of an undergraduate and much of a graduate mathematics curriculum. Nothing about design-based inference is in it. Everything design-based inference is made of is: Finset, ∑, ℝ, Nat.choose, order, algebra.

Two properties make it navigable. It has a naming convention strict enough that names are predictable from statements, and it has search tools that work on shapes rather than words.

Names are generated from statements

Reading a nameNew tab

#check @mul_comm
#check @add_div
#check @Finset.sum_add_distrib
#check @Nat.cast_sub
#check @sq_nonneg

The rule is: describe the left-hand side of the conclusion, in order, using the standard word for each operation, in snake_case, prefixed by the namespace of the type it is about.

mul_comm — a * b = b * a. Multiplication, commutativity.
add_div — (a + b) / c = a / c + b / c. The name describes the left-hand side: an addition inside a division.
Finset.sum_add_distrib — inside the Finset namespace, a sum of a sum distributes.
Nat.cast_sub — the coercion ℕ → ℝ pushed through a subtraction.

Suffixes are equally regular: _nonneg (0 ≤ _), _pos (0 < _), _ne_zero, _le, _lt, _iff (an ↔), _of_ (takes a hypothesis, as in Nat.sub_lt_of_lt), _eq_ (a rewriting lemma), ' (a variant, usually with different hypotheses).

Two consequences. First, you can often guess a name: “the sum of nonnegative things is nonnegative, over a Finset” is Finset.sum_nonneg, and it is. Second — more useful when reading — you can predict a statement from a name, which means you can read a proof and follow the argument without looking anything up. That is what makes a Mathlib proof readable in a way that, say, a Coq proof script usually is not.

Names also drift. div_add_div_same was a / c + b / c = (a + b) / c for years; the same fact is now add_div, stated in the other direction. This is the main reason a proof that compiled a year ago may not compile today, and the main reason to reach for exact? rather than memory.

Reading a statement

#check @foo prints foo’s statement with every argument made explicit, including the ones normally inferred. It is the only reliable way to see what a lemma actually requires.

#check @Finset.sum_le_sumNew tab

#check @Finset.sum_le_sum
#check @Finset.sum_nonneg

Lean has three kinds of argument, and the brackets tell you which is which:

(x : α) — explicit. You supply it, positionally.
{x : α} — implicit. Lean infers it by unifying the rest of the statement with the goal. Types and index sets are usually implicit, because they are determined by the other arguments.
[inst : Foo α] — instance implicit, or typeclass argument. Lean searches its database of registered instances for a value. This is how ” $α$ is a commutative ring” gets said.

So in

@Finset.sum_le_sum :
  ∀ {ι : Type u_1} {N : Type u_2} [inst : AddCommMonoid N] [inst_1 : Preorder N]
    {f g : ι → N} {s : Finset ι} [AddLeftMono N],
    (∀ i ∈ s, f i ≤ g i) → ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i

there is exactly one thing you have to provide: a proof of ∀ i ∈ s, f i ≤ g i. Everything else is found.

Three details in that display are worth pausing on, because each is somewhere a formalization can go quietly wrong.

The typeclass arguments are the mathematical setting. AddCommMonoid N, Preorder N, AddLeftMono N — a commutative additive monoid with a compatible preorder. ℝ satisfies all three. So does ℕ. So does ℝ≥0∞, where subtraction truncates and $\infty - \infty = 0$ . A statement that reads correctly in $R$ may be about a structure with different arithmetic, and the type is the only place that shows.

∀ i ∈ s is not ∀ i. ∀ i ∈ s, f i ≤ g i unfolds to ∀ i, i ∈ s → f i ≤ g i. If you have a hypothesis of the form ∀ i, f i ≤ g i, exact h will fail and the error will be about a mismatch you cannot see. This is the single most common beginner confusion.

LemmaSupplying a bounded hypothesis

A pointwise bound over all units is stronger than the bound over s that Finset.sum_le_sum asks for, so it can be adapted — but not by exact h. The adapter is fun i _ => h i: take the unit i, discard the unused proof that i ∈ s, and return h i. When you see that idiom in somebody’s proof, it is almost always this mismatch being absorbed.

New tab

example {ι : Type} (s : Finset ι) (f g : ι → ℝ) (h : ∀ i, f i ≤ g i) :
    ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i :=
  Finset.sum_le_sum fun i _ => h i

u_1 and u_2 are universe variables. They are the mechanism that keeps “the type of all types” from being a type of itself. You can ignore them entirely; they never carry mathematical content in ordinary work, and they are noise in every #check output for the rest of your life.

`open`, and why a statement can mean different things in different files

open, and dot notation as namespace resolutionNew tabOpens with 43 lines of library preamble — the code above is at the bottom of the editor.

#check @Finset.card_univ

theorem count_units (z : Assignment n) : (#z : ℝ) = (z.card : ℝ) := rfl

theorem tau_dot (P : Population n) : P.tau = Population.tau P := rfl

open Finset makes every name in the Finset namespace available unqualified, so sum_add_distrib resolves to Finset.sum_add_distrib and the notation #s means s.card. It changes nothing about the library and everything about what a given piece of text means.

That is worth stating as a warning rather than a convenience. A formal statement is not self-contained: the same characters resolve to different constants depending on what is open where they appear. When you are handed a theorem to audit and it arrives as a screenshot or a chat message, the open lines and the enclosing namespace are part of the statement, and you have not been given them. Ask for the file.

Dot notation is the same phenomenon in miniature: P.tau is Population.tau P, found because P : Population n. Chapter 4 covered the rule; the point here is that it is name resolution, so P.tau means whatever Population.tau means in that file, and #print Population.tau is how you find out.

Looking under the hood

Three commands, all one line, all worth running before you believe anything. The theorem they are demonstrated on is a real one, small enough to check by eye.

Claim. Under the sharp null of no effect — $y_{1} (i) = y_{0} (i)$ for every unit $i$ — the average treatment effect is zero.

Proof.

Every individual effect $y_{1} (i) - y_{0} (i)$ is zero, so the sum of them over the $n$ units is zero, and $τ = 0 / n = 0$ .∎

#print and #print axiomsNew tabOpens with 49 lines of library preamble — the code above is at the bottom of the editor.

#print Population.tau

theorem tau_of_no_effect (P : Population n) (h : ∀ i, P.y1 i = P.y0 i) : P.tau = 0 := by
  have hz : ∀ i, P.y1 i - P.y0 i = 0 := fun i => by rw [h i, sub_self]
  simp only [Population.tau, hz, Finset.sum_const_zero, zero_div]

#print axioms tau_of_no_effect

#check @thm — the statement, fully explicit. What the theorem says.
#print f — a definition’s body. What the words in the statement mean.
#print axioms thm — everything the proof transitively rests on. Whether the proof is a proof.

#print axioms on an ordinary theorem reports exactly three names:

'tau_of_no_effect' depends on axioms: [propext, Classical.choice, Quot.sound]

propext (propositions that imply each other are equal), Classical.choice (the axiom of choice, which gives excluded middle and is used in the construction of ℝ itself) and Quot.sound (quotients respect their relation; ℝ, ℚ, ℤ and Finset are all built from quotients). Those three are the baseline. Anything else in that list is a fact about the proof you were not told.

That output is from the theorem in the block above, whose own proof is worth reading too — it is the two informal sentences, one line each.

```
have hz : ∀ i, P.y1 i - P.y0 i = 0 := fun i => by rw [h i, sub_self]
```
The hypothesis is stated as an equality of outcomes and the estimand is built from their difference, so the first line converts one into the other. Its proof is a function of the unit: at each i, rw [h i] replaces P.y1 i by P.y0 i, leaving P.y0 i - P.y0 i = 0, and sub_self : a - a = 0 is that equation — rewriting with it makes both sides 0 and closes the goal.
```
simp only [Population.tau, …]
```
Naming the definition unfolds it, so the goal becomes (∑ i, (P.y1 i - P.y0 i)) / ↑n = 0. Then hz, used as a rewrite rule, fires inside the sum: every summand becomes 0, as shown below. A ∀-hypothesis in a simp only list is used this way constantly — it is one rewrite per index, applied everywhere at once.
Goal
```
n : ℕ
P : Population n
h : ∀ (i : Fin n), P.y1 i = P.y0 i
hz : ∀ (i : Fin n), P.y1 i - P.y0 i = 0
⊢ (∑ x, 0) / ↑n = 0
```

Finset.sum_const_zero

Finset.sum_const_zero : ∑ _i ∈ s, 0 = 0. Adding up zeros gives zero, for any index set and without needing to know how many there are.

Goal

n : ℕ
P : Population n
h : ∀ (i : Fin n), P.y1 i = P.y0 i
hz : ∀ (i : Fin n), P.y1 i - P.y0 i = 0
⊢ 0 / ↑n = 0

```
zero_div
```
zero_div : 0 / a = 0 finishes, and note that it holds for every a, including a = 0 — this is one of the places where the division convention saves a hypothesis rather than costing one. The theorem needs no 0 < n, and correctly so: at $n = 0$ there is nothing to average and $τ$ is $0$ anyway.

Finding a lemma

The example below proves that a sum of squares is non-negative, $\sum_{i = 1}^{n} v_{i}^{2} \geq 0$ : each term is a square, hence non-negative, and a finite sum of non-negative terms is non-negative. Both halves of that sentence are Mathlib lemmas, and the point of this section is how you would have found them.

exact?, Loogle, Moogle, the docsNew tabOpens with 57 lines of library preamble — the code above is at the bottom of the editor.

theorem sum_nonneg_example (v : Fin n → ℝ) : 0 ≤ ∑ i, (v i) ^ 2 := by
  exact Finset.sum_nonneg fun i _ => sq_nonneg (v i)

```
exact Finset.sum_nonneg fun i _ => sq_nonneg (v i)
```
Finset.sum_nonneg : (∀ i ∈ s, 0 ≤ f i) → 0 ≤ ∑ i ∈ s, f i is the second half of the sentence. It wants one argument: a proof that every summand is non-negative, in the ∀ i ∈ s shape discussed above, so the argument is fun i _ => … — take the unit, discard the proof that it is in the index set, and produce the bound. That bound is sq_nonneg (v i) : 0 ≤ v i ^ 2, the first half. One term, two lemmas, no tactics.

Neither name had to be remembered. exact? on this goal returns the whole term; failing that, the conventions of the previous section predict Finset.sum_nonneg and sq_nonneg from the statements they would have to have. In rough order of what to try:

exact? searches for a single existing lemma that closes the current goal, and prints it as Try this: exact …. It is slow — seconds, sometimes tens of seconds — and it knows the entire library, which no human does. apply? is the version that accepts a lemma leaving goals behind.
simp? runs simp and then prints the simp only [...] call that would have done the same thing. This is how you convert a fragile bare simp into the explicit list the library style guide asks for, and how you find out what simp actually did when it closed a goal you did not understand. rw? offers the rewrites that apply to the goal.
Guess the name from the conventions above; the editor’s autocompletion will confirm or deny in a keystroke.
Loogle searches by shape. Typing Finset.sum, _ * _ returns the lemmas whose statements mention both a Finset.sum and a product. This is the right tool when you know what the mathematics looks like and not what it is called — which, when reading somebody else’s formalization, is most of the time. Moogle does the same job from a natural-language description.
The Mathlib docs, generated from the source, always current, and searchable.

Part two: the audit checklist

Now the substance. Below are seven ways an autoformalized statement goes wrong while compiling, each presented as a pair: a statement that looks right and is right, and a statement that looks right and is not. Every one of the wrong ones is a theorem — Lean accepts it, and it is here because it compiles.

The running example is the miniature library from chapter 4, plus the difference-in-means estimator:

The estimator the audits are aboutNew tab

noncomputable def DiM (P : Population n) (z : Assignment n) : ℝ :=
  (∑ i ∈ z, P.y1 i) / (#z : ℝ) - (∑ i ∈ zᶜ, P.y0 i) / (#zᶜ : ℝ)

Definition. Given an assignment $z$ treating $n_{1} = | z |$ of the $n$ units, the difference in means is the average treated outcome among the treated units minus the average control outcome among the rest:

\hat{τ} (z) = \frac{1}{n_{1}} \sum_{i \in z} y_{1} (i) - \frac{1}{n_{0}} \sum_{i \notin z} y_{0} (i), n_{0} = n - n_{1} .

Each unit contributes the one potential outcome the assignment reveals, which is what makes this a statistic rather than a function of unobservables. Note that no hypothesis excludes $n_{1} = 0$ or $n_{0} = 0$ : by the division convention the estimator is defined at those assignments too, and the check on denominators below is about what it is defined to be.

1. Are the hypotheses satisfiable?

A hypothesis set that nothing satisfies proves everything. This is the oldest trap in formalization and it survives autoformalization intact, because a model that generates a plausible-sounding side condition has no obligation to check that any object meets it.

Right:

A hypothesis that is doing workNew tabOpens with 60 lines of library preamble — the code above is at the bottom of the editor.

theorem good_mean_const (hn : 0 < n) (c : ℝ) : mean (fun _ : Fin n => c) = c := by
  have hn' : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn.ne'
  simp only [mean, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  field_simp

0 < n is satisfiable — take $n = 1$ — and it is needed, because at $n = 0$ the mean is $0 / 0 = 0$ and the statement is false for $c \neq 0$ . The proof is chapter 3’s warm-up, and it spends the hypothesis in exactly one place.

```
have hn' : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn.ne'
```
The hypothesis arrives as 0 < n in ℕ and is needed as (n : ℝ) ≠ 0. hn.ne' turns 0 < n into n ≠ 0 (.ne would give 0 ≠ n, the wrong way round), and Nat.cast_ne_zero : (↑n ≠ 0) ↔ (n ≠ 0) carries that across the coercion, right to left.
```
simp only [mean, Finset.sum_const, …]
```
Unfold mean, then the four-rewrite dance from chapter 3: Finset.sum_const turns the sum of c over the units into #univ • c, Finset.card_univ and Fintype.card_fin turn the count into n, and nsmul_eq_mul turns the scalar action into a product. The goal is now the cancellation shown below.
Goal
```
n : ℕ
hn : 0 < n
c : ℝ
hn' : ↑n ≠ 0
⊢ ↑n * c / ↑n = c
```
```
field_simp
```
field_simp finds hn' in the context, cancels the ↑n, and closes the goal. That is the one place the hypothesis is used — which is what “the hypothesis is doing work” means, and what you should be able to point at for every hypothesis in a statement you are auditing.

Wrong:

ExerciseVacuous hypotheses (warm-up)

The statement claims every population has zero average treatment effect, “assuming” $0 < n_{1} < 0$ . Nothing in $N$ satisfies that, so the theorem holds vacuously and says nothing at all. Prove it anyway.

The check that would have caught it is no_such_n₁, below the exercise: state the negation of the hypothesis set and try to prove it. If you succeed, the theorem is empty. Notice this is not a heuristic — it is a Lean statement, and the compiler will settle it.

New tabOpens with 65 lines of library preamble — the code above is at the bottom of the editor.

theorem bad_vacuous (n₁ : ℕ) (h : 0 < n₁ ∧ n₁ < 0) (P : Population n) : P.tau = 0 := by
  sorry

theorem no_such_n₁ : ¬ ∃ k : ℕ, 0 < k ∧ k < 0 := by
  rintro ⟨k, h1, h2⟩
  omega

Hint

Two tactics. exfalso replaces the goal by False — anything follows from a contradiction, so proving False proves the goal — and omega, a decision procedure for linear arithmetic over ℕ and ℤ, finds the contradiction in h immediately.

Show solution

New tabOpens with 65 lines of library preamble — the code above is at the bottom of the editor.

theorem bad_vacuous (n₁ : ℕ) (h : 0 < n₁ ∧ n₁ < 0) (P : Population n) : P.tau = 0 := by
  exfalso
  omega

theorem no_such_n₁ : ¬ ∃ k : ℕ, 0 < k ∧ k < 0 := by
  rintro ⟨k, h1, h2⟩
  omega

The habit: for every theorem you are asked to trust, either exhibit one object satisfying all the hypotheses, or prove that none exists. In practice the first is usually easy and is the more informative of the two, because it tells you which objects the theorem is about.

2. Is the type right?

Sample sizes are naturals. Outcomes, estimates and estimands are reals. When those get mixed up the statement stays true and stops being about your data, because ℕ arithmetic is not the arithmetic you have in mind: subtraction truncates at zero and division floors.

Right:

Counts in ℕ, arithmetic in ℝNew tabOpens with 73 lines of library preamble — the code above is at the bottom of the editor.

theorem good_group_sizes (m k : ℕ) (h : k ≤ m) : (k : ℝ) + ((m - k : ℕ) : ℝ) = m := by
  rw [Nat.cast_sub h]
  ring

Group sizes are counted in ℕ and then cast. The claim is the obvious one — the treated and control groups partition the sample, so $n_{1} + n_{0} = n$ — and the only reason it takes two lines is the boundary between the two number types.

```
rw [Nat.cast_sub h]
```
Nat.cast_sub : k ≤ m → ((m - k : ℕ) : ℝ) = ↑m - ↑k moves the subtraction across the cast, and — this is the part that matters — it requires k ≤ m, supplied here as h. Without that hypothesis the equation is false, since ℕ-subtraction truncates at zero.
Goal
```
m k : ℕ
h : k ≤ m
⊢ ↑k + (↑m - ↑k) = ↑m
```
```
ring
```
What is left, ↑k + (↑m - ↑k) = ↑m, is subtraction in ℝ, where it behaves, so ring closes it. If you ever see a formalization casting a difference of counts without a proof of the corresponding inequality, either the inequality is hiding somewhere or the statement is wrong.

Wrong:

Exerciseℕ truncation (warm-up)

“Treatment never harms anybody”, over ℕ. It is true — and it is true of every pair of outcome vectors, including ones where treatment halves every outcome, because 3 - 5 = 0 in ℕ. The statement is not false; it is about a different arithmetic. Prove it.

The two #evals below the theorem make the point concrete. If the outcomes in a formalization you are auditing live in ℕ, stop reading and ask why.

New tabOpens with 77 lines of library preamble — the code above is at the bottom of the editor.

theorem bad_nat_effect (y1 y0 : Fin 3 → ℕ) (i : Fin 3) : 0 ≤ y1 i - y0 i := by
  sorry

#eval (3 : ℕ) - 5
#eval (3 : ℤ) - 5

Hint

One lemma from the Nat namespace: exact Nat.zero_le _. In ℕ every value is ≥ 0, whatever the subtraction did, which is exactly why the theorem is empty.

Show solution

New tabOpens with 77 lines of library preamble — the code above is at the bottom of the editor.

theorem bad_nat_effect (y1 y0 : Fin 3 → ℕ) (i : Fin 3) : 0 ≤ y1 i - y0 i := by
  exact Nat.zero_le _

#eval (3 : ℕ) - 5
#eval (3 : ℤ) - 5

This one has a specific tell. In ℕ, 0 ≤ x is provable for every x by Nat.zero_le, so any statement of the form “some ℕ-valued expression is non-negative” is content-free. More generally: if a proof is one lemma long and that lemma’s name mentions the type rather than the mathematics, the type is doing the work.

Chapter 7’s complete-randomization formulas are stated with real subtraction on the right-hand side, $(n_{1} : R) - 1$ , for exactly this reason: in ℕ, $n_{1} - 1$ is $0$ at $n_{1} = 0$ and $n_{1} - 2$ is $0$ at $n_{1} = 1$ , so a natural-number statement of those formulas would be about truncated quantities at precisely the degenerate designs it is supposed to cover.

3. Where are the denominators?

Lean’s x / 0 = 0 is a convention that makes every division total. It is a good convention — chapter 4 explained why the library leans on it — and it means a claim about a ratio is automatically true wherever the denominator vanishes.

Claim. Let $z$ be an assignment that treats at least one unit. Then the treated-group mean times the number of treated units recovers the treated-group total:

(\frac{1}{n_{1}} \sum_{i \in z} y_{1} (i)) \cdot n_{1} = \sum_{i \in z} y_{1} (i), n_{1} = | z | \geq 1 .

Proof.

Since at least one unit is treated, $n_{1} \geq 1$ , so $n_{1} \neq 0$ and the division cancels.∎

Right:

Non-emptiness stated where it belongsNew tabOpens with 83 lines of library preamble — the code above is at the bottom of the editor.

theorem good_treated_mean (P : Population n) (z : Assignment n) (hz : z.Nonempty) :
    (∑ i ∈ z, P.y1 i) / (#z : ℝ) * (#z : ℝ) = ∑ i ∈ z, P.y1 i := by
  have : (#z : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (Finset.card_ne_zero_of_mem hz.choose_spec)
  field_simp

The whole of that one-line informal proof is the have, and the interesting part is how “at least one unit is treated” becomes “the denominator is not zero”.

```
have : (#z : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (Finset.card_ne_zero_of_mem hz.choose_spec)
```
Read the term from the inside out. hz : z.Nonempty unfolds to ∃ i, i ∈ z, and hz.choose_spec is the proof that the witness that existential provides really is a member of z — choose names the witness, choose_spec is its property, and together they are how you get a concrete element out of an existential in term mode. Then Finset.card_ne_zero_of_mem : a ∈ s → #s ≠ 0 says a set with a member is not empty, and Nat.cast_ne_zero.mpr carries #z ≠ 0 across the coercion into ℝ. The fact is unnamed — have : with no name binds it as this — because only the next line uses it. Its statement is what appears in the context below.
Goal
```
n : ℕ
P : Population n
z : Assignment n
hz : Finset.Nonempty z
this : ↑(#z) ≠ 0
⊢ (∑ i ∈ z, P.y1 i) / ↑(#z) * ↑(#z) = ∑ i ∈ z, P.y1 i
```
```
field_simp
```
With the non-vanishing fact in context, field_simp cancels the ↑(#z) and the goal closes.

Wrong:

ExerciseDivision by zero (core)

The difference in means at the assignment that treats nobody. The treated average is $0 / 0 = 0$ , so DiM P ∅ is minus the control mean — and the leading $0$ is not an estimate of anything.

The reason to care: a design supported entirely on degenerate assignments satisfies many plausible-looking identities for this reason and no other. When auditing, list every / in the statement and ask, for each, what makes the denominator non-zero and where that fact is recorded.

New tabOpens with 88 lines of library preamble — the code above is at the bottom of the editor.

theorem bad_div_zero (P : Population n) : DiM P ∅ = - (∑ i, P.y0 i) / n := by
  sorry

Hint

One simp only, with DiM unfolded and the lemma list from the docstring: Finset.sum_empty, Finset.card_empty and Nat.cast_zero make the treated term 0 / 0, div_zero — the one that matters — makes it 0, and zero_sub with neg_div puts what is left in the stated form.

Show solution

New tabOpens with 88 lines of library preamble — the code above is at the bottom of the editor.

theorem bad_div_zero (P : Population n) : DiM P ∅ = - (∑ i, P.y0 i) / n := by
  simp only [DiM, Finset.sum_empty, Finset.card_empty, Nat.cast_zero, div_zero,
    Finset.compl_empty, Finset.card_univ, Fintype.card_fin, zero_sub, neg_div]

4. Are the quantifiers in the right order?

The example is the oldest $ε$ – $N$ statement there is.

Proposition. For every $ε > 0$ there is a natural number $N$ with $1 / (N + 1) < ε$ .

Proof.

The reals are Archimedean: no real number bounds every natural number. So there is an $N$ with $N + 1 > 1 / ε$ , and since both sides are positive, taking reciprocals gives $1 / (N + 1) < ε$ .∎

The order of the two quantifiers is the content. $N$ is chosen after $ε$ is known, and is allowed to depend on it — which is why no single $N$ has to work for all tolerances.

Right:

∀ ε, ∃ NNew tabOpens with 92 lines of library preamble — the code above is at the bottom of the editor.

theorem good_quantifier_order : ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, (1 : ℝ) / (N + 1) < ε :=
  fun _ hε => exists_nat_one_div_lt hε

```
fun _ hε => …
```
The statement is ∀ ε, 0 < ε → ∃ N, …, and chapter 1 established that both a ∀ and an → are introduced by fun. So the proof is a function of two arguments: the tolerance, written _ because nothing in the body names it, and the proof hε that it is positive. The dependence of $N$ on $ε$ is visible right here — whatever is returned is computed inside a function that has already been given $ε$ .
```
exists_nat_one_div_lt hε
```
Mathlib’s exists_nat_one_div_lt : 0 < ε → ∃ n : ℕ, 1 / (↑n + 1) < ε is the Archimedean property in exactly this shape, so applying it to hε is the whole proof. Two details in its statement are deliberate: the + 1 in the denominator means the witness may be 0 and no division by zero can arise, and the ↑n is the coercion ℕ → ℝ, because the witness is a natural number and the inequality is about reals.

Wrong:

ExerciseQuantifier order (core)

Swap the two and you get “one sample size works for every tolerance”, which is a different and false claim. Autoformalizers swap these routinely, partly because English is ambiguous about it and partly because the swapped version reads more tidily.

The exercise asks you to refute it: show that no single $N$ works for every $ε$ .

New tabOpens with 95 lines of library preamble — the code above is at the bottom of the editor.

theorem bad_quantifier_order : ¬ ∃ N : ℕ, ∀ ε : ℝ, 0 < ε → (1 : ℝ) / (N + 1) < ε := by
  sorry

Hint

rintro ⟨N, h⟩ introduces the hypothetical N together with its property — rintro is intro plus destructuring, so it takes the existential apart in one step. Then feed h the tolerance $ε = 1 / (N + 1)$ , which is positive by positivity, and it asserts $1 / (N + 1) < 1 / (N + 1)$ , which lt_irrefl refutes.

Show solution

New tabOpens with 95 lines of library preamble — the code above is at the bottom of the editor.

theorem bad_quantifier_order : ¬ ∃ N : ℕ, ∀ ε : ℝ, 0 < ε → (1 : ℝ) / (N + 1) < ε := by
  rintro ⟨N, h⟩
  have hpos : (0 : ℝ) < 1 / (N + 1) := by positivity
  exact absurd (h _ hpos) (lt_irrefl _)

Nothing about this is specific to asymptotics; it is just where the failure is most familiar. The same swap in this subject would be “there is a design under which every population’s difference in means is unbiased” versus “for every population there is such a design” — the first is a claim about experimental design, the second is nearly vacuous.

Read quantifiers outside in, and say them aloud in English. If the English is ambiguous, that is the thing to fix, not the Lean.

5. Is a definition doing the theorem’s work?

This is the failure that survives every other check, because the statement, the hypotheses and the proof are all fine. The problem is upstream: one of the words means something other than what you assumed.

Right:

An estimand that does not know about the assignmentNew tabOpens with 100 lines of library preamble — the code above is at the bottom of the editor.

theorem good_estimand (P : Population n) :
    P.tau = (∑ i, (P.y1 i - P.y0 i)) / n := rfl

$τ$ is a function of the potential outcomes alone. It does not take an assignment, so a theorem relating an estimator to it has something to say.

Wrong:

ExerciseA definition that bakes in the conclusion (warm-up)

Here the “estimand” is defined to be the estimator. Unbiasedness is then true by definition, and the proof is one word — which is the tell, and the exercise.

Two mechanical checks would have caught it. The estimand takes z as an argument, and no estimand should: an estimand is a property of the population, which is exactly why the type Population n → ℝ is the right one and Population n → Assignment n → ℝ is not. And #print tauCircular shows the body, which is one line long and contains the estimator’s name.

New tabOpens with 103 lines of library preamble — the code above is at the bottom of the editor.

noncomputable def tauCircular (P : Population n) (z : Assignment n) : ℝ := DiM P z

theorem bad_circular_target (P : Population n) (z : Assignment n) :
    DiM P z = tauCircular P z := by
  sorry

#print tauCircular

Hint

rfl. tauCircular P z unfolds to DiM P z, so the two sides of the equation are the same term and there is nothing to prove.

Show solution

New tabOpens with 103 lines of library preamble — the code above is at the bottom of the editor.

noncomputable def tauCircular (P : Population n) (z : Assignment n) : ℝ := DiM P z

theorem bad_circular_target (P : Population n) (z : Assignment n) :
    DiM P z = tauCircular P z := by
  rfl

#print tauCircular

A rfl proof of a substantive-sounding claim is always worth a second look. It means the two sides reduce to the same term, i.e. that the claim is a change of notation. Sometimes that is exactly right and worth stating. When the claim is “this estimator is unbiased”, it never is.

6. What does the proof rest on?

sorry, axiom, and #print axiomsNew tabOpens with 111 lines of library preamble — the code above is at the bottom of the editor.

theorem clean_proof (x : ℝ) : 0 ≤ x ^ 2 + 1 := by positivity

#print axioms clean_proof

clean_proof is the baseline: one positivity call on $0 \leq x^{2} + 1$ , a sum of a square and a positive constant, and #print axioms on it reports the three standard names and nothing else. Everything below is about what shows up in that list when the proof is not what it appears to be.

sorry closes any goal. It is the honest way to leave a hole, and Lean emits a warning when you use it — but the warning is emitted where the sorry is, not where the finished theorem is used. A helper lemma three files away, proved by sorry, produces a headline theorem that compiles with no warning at its own definition site and is worth nothing.

#print axioms is the check, and it is not foolable, because sorry is implemented as an axiom (sorryAx) and axioms propagate through the proof term:

'uses_sorried' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]

A declared axiom behaves the same way and is worse, because no warning is ever emitted at all — an axiom is a legitimate feature, and the file looks clean:

axiom key_step (x : ℝ) : x ≤ x + 1
theorem helper (x : ℝ) : x - 1 ≤ x := by have := key_step (x - 1); linarith
#print axioms helper

Lean reports that helper depends on key_step (along with standard logical axioms used by Mathlib). The theorem is therefore only as strong as the declared axiom.

Three further names to recognize in that output:

sorryAx — a hole. The theorem is not proved.
Lean.ofReduceBool (accompanied, in recent Lean versions, by Lean.trustCompiler) — the proof used native_decide, which evaluates a decidable proposition by compiling it to machine code and running it. That trusts the Lean compiler and your CPU in a way the kernel does not. It is not necessarily wrong; it is a different and much larger trusted base, and it should be a deliberate choice rather than a surprise.
anything else — a project-specific axiom. Read it. It may be a reasonable modeling assumption stated as an axiom, or it may be the theorem.

Run #print axioms on the headline result of every formalization you did not write. It costs one line.

7. Is `decide` proving a theorem or an instance?

Right:

A finite check that really is finiteNew tabOpens with 115 lines of library preamble — the code above is at the bottom of the editor.

theorem good_decide : ∀ i : Fin 3, i.val < 3 := by decide

decide proves a goal by evaluating a decision procedure for it. When the goal genuinely is a finite check — a property of the three units of a three-unit study — this is exactly right, and it is one of the pleasant things about a finite-population subject: many statements really are decidable.

Wrong:

Exercisedecide on the small instance (core)

$k^{2} \leq 2^{k}$ , checked for $k < 3$ . The check succeeds, and the claim is false at $k = 3$ : $9 > 8$ . Prove both statements.

The moral is narrow and important: a decide proof establishes exactly the instances it enumerated. A statement quantified over a bound that happens to be small, proved by decide, tells you nothing about the general case — and the bound is easy to miss when it is buried in the binder.

New tabOpens with 117 lines of library preamble — the code above is at the bottom of the editor.

theorem bad_decide_small : ∀ k < 3, k ^ 2 ≤ 2 ^ k := by
  sorry

theorem bad_decide_fails : ¬ (3 ^ 2 ≤ 2 ^ 3) := by
  sorry

Hint

decide proves both, one tactic each: for the first it enumerates k = 0, 1, 2, and for the second it evaluates 3 ^ 2 ≤ 2 ^ 3 to false. That the same tactic settles the claim and its counterexample is the point.

Show solution

New tabOpens with 117 lines of library preamble — the code above is at the bottom of the editor.

theorem bad_decide_small : ∀ k < 3, k ^ 2 ≤ 2 ^ k := by
  decide

theorem bad_decide_fails : ¬ (3 ^ 2 ≤ 2 ^ 3) := by
  decide

The same applies to norm_num and native_decide on parametrized claims, and to simp when the simp set contains a lemma that only fires for small numerals. When a proof is one tactic long and the statement is about a family, find out which member of the family was checked.

The checklist

The checklist, in orderNew tabOpens with 123 lines of library preamble — the code above is at the bottom of the editor.

theorem checklist_placeholder : True := trivial

Two remarks on order. Reading the conclusion alone comes first because it is free and it catches the largest class of errors: a statement about the wrong object. Checking satisfiability comes second because a vacuous theorem defeats every subsequent check — it will pass all of them.

And one remark on item 3. An unused hypothesis is not by itself an error; a theorem may be stated with a hypothesis for uniformity with its neighbor. But it is always a question worth asking, because there are only two answers: the theorem is stronger than advertised (good, and you should restate it), or the work you expected that hypothesis to do is being done somewhere you have not looked (bad).

The audit exercise

Everything above was a single flaw in isolation. Here is one that looks like a real theorem.

The prompt was: “under a design that assigns a fixed number of units to treatment, the difference in means is unbiased for the average treatment effect.” The output compiles, and it is the sort of thing that would pass a skim.

ExerciseAudit this (core)

Prove it first. Writing the proof is how you find the flaw, because the proof never touches anything specific about DiM, tau, or the design.

Then, before reading on: what is wrong with it as a formalization of unbiasedness?

New tabOpens with 125 lines of library preamble — the code above is at the bottom of the editor.

theorem ex_DiM_unbiased_audit (D : Design n) (P : Population n)
    (hbal : ∀ z, D.prob z ≠ 0 → DiM P z = P.tau) :
    D.expect (DiM P) = P.tau := by
  sorry

Hint

First establish, for each z, that D.prob z * DiM P z = D.prob z * P.tau, by by_cases hz : D.prob z = 0: in the zero branch both sides are 0 * _, and off the null set hbal z hz rewrites DiM P z to P.tau. Then unfold Design.expect, apply that fact with Finset.sum_congr rfl, and the sum ∑ z, D.prob z * P.tau collapses under ← Finset.sum_mul, D.sum_one and one_mul.

Show solution

New tabOpens with 125 lines of library preamble — the code above is at the bottom of the editor.

theorem ex_DiM_unbiased_audit (D : Design n) (P : Population n)
    (hbal : ∀ z, D.prob z ≠ 0 → DiM P z = P.tau) :
    D.expect (DiM P) = P.tau := by
  have key : ∀ z ∈ (Finset.univ : Finset (Assignment n)),
      D.prob z * DiM P z = D.prob z * P.tau := by
    intro z _
    by_cases hz : D.prob z = 0
    · rw [hz, zero_mul, zero_mul]
    · rw [hbal z hz]
  simp only [Design.expect]
  rw [Finset.sum_congr rfl key, ← Finset.sum_mul, D.sum_one, one_mul]

ExerciseThe flaw, and how to see it (stretch)

The docstring states the answer; the exercise is to prove the sharp version of it: under hbal the estimator has zero variance, $E [(\hat{τ} - τ)^{2}] = 0$ .

New tabOpens with 137 lines of library preamble — the code above is at the bottom of the editor.

theorem ex_hbal_forces_zero_variance (D : Design n) (P : Population n)
    (hbal : ∀ z, D.prob z ≠ 0 → DiM P z = P.tau) :
    D.expect (fun z => (DiM P z - P.tau) ^ 2) = 0 := by
  sorry

Hint

Reuse the argument you just wrote with (DiM P z - P.tau) ^ 2 in place of DiM P z: the same by_cases hz : D.prob z = 0 shows every summand D.prob z * (DiM P z - P.tau) ^ 2 is 0 — off the null set hbal z hz and sub_self leave _ * 0 ^ 2, which ring clears. After Finset.sum_congr rfl the sum is of a constant 0, and Finset.sum_const with smul_zero finishes.

Show solution

New tabOpens with 137 lines of library preamble — the code above is at the bottom of the editor.

theorem ex_hbal_forces_zero_variance (D : Design n) (P : Population n)
    (hbal : ∀ z, D.prob z ≠ 0 → DiM P z = P.tau) :
    D.expect (fun z => (DiM P z - P.tau) ^ 2) = 0 := by
  have key : ∀ z ∈ (Finset.univ : Finset (Assignment n)),
      D.prob z * (DiM P z - P.tau) ^ 2 = 0 := by
    intro z _
    by_cases hz : D.prob z = 0
    · rw [hz, zero_mul]
    · rw [hbal z hz, sub_self]
      ring
  simp only [Design.expect]
  rw [Finset.sum_congr rfl key, Finset.sum_const, smul_zero]

The flaw is item 7 on the checklist, in its realistic form. hbal says the estimator equals the estimand at every assignment the design can produce. That is not unbiasedness — it is exactness. Unbiasedness is a statement about an average, and its entire content is that DiM may be wrong at every single assignment provided the errors cancel. Here that content has been moved into a hypothesis, and what remains of the theorem is linearity of expectation.

Three tells, all mechanical, none requiring you to know what the right theorem looks like:

The hypothesis mentions both the estimator and the estimand. A hypothesis about a design should be a statement about the design: “assigns exactly $n_{1}$ units”, “every propensity is positive”. hbal relates DiM to tau, which is what the conclusion is supposed to do. Whenever a hypothesis and the conclusion mention the same pair of objects, suspect that the hypothesis contains the conclusion.
The design is arbitrary. The informal statement says “a fixed number of units to treatment”. n₁ does not appear in the formalization at all; neither does completeRandomization, nor any support condition. A formalization that drops a named condition from the prompt has either found it unnecessary — in which case the theorem should be stronger, and it is worth asking how — or replaced it with something else.
hbal is unsatisfiable for any interesting population. The second exercise proves the precise version: under hbal, $E [(\hat{τ} - τ)^{2}] = 0$ , so the estimator has zero variance. Since DiM has strictly positive variance under complete randomization whenever the potential outcomes vary, hbal holds only in degenerate cases. This is check 2 — satisfiability — applied not to the hypothesis in isolation but to the hypothesis together with the situation the theorem claims to describe.

The correct statement is DiM_unbiased_completeRandomization, and you will meet it in chapter 8:

theorem DiM_unbiased_completeRandomization {n₁ : ℕ} (hle : n₁ ≤ n) (P : Population n)
    (hpos : 0 < n₁) (hlt : n₁ < n) :
    (completeRandomization n n₁ hle).expect (DiM P) = P.tau

Compare the hypotheses. hle, hpos, hlt are all conditions on $n_{1}$ — a number the experimenter chooses — and none of them mentions DiM or tau. The design is named. P is arbitrary. That is what an unbiasedness statement looks like, and its proof is a good deal longer than five lines, because it has something to do.

Reading autoformalized Lean

Two more, in the style of the chapter itself: statements about reading, where the flaw is in what the notation resolves to rather than in what it says.

The name is not the meaning

namespace Mine
noncomputable def mean (v : Fin n → ℝ) : ℝ := (∑ i, v i) / (n - 1)
end Mine

open Mine in
theorem mean_of_const_bad (hn : 1 < n) (c : ℝ) :
    mean (fun _ : Fin n => c) = c * n / (n - 1) := …

The statement uses mean, and mean is the name this tutorial’s library gives to $(1 / n) \sum_{i} v_{i}$ . Here an open Mine has put a different mean in scope — one dividing by $n - 1$ — and the theorem is a true statement about that one. Nothing is hidden and nothing is dishonest; the reader simply resolved a name differently from the elaborator.

This is why an audit starts by #printing every definition the statement mentions, and why a statement pasted without its file header cannot be audited at all. When a formalization arrives as a fragment, the first question is not “is this right” but “what is in scope”.

A proof that trusts your CPU

theorem euler_polynomial_is_prime : ∀ k < 40, Nat.Prime (k ^ 2 + k + 41) := by
  native_decide

native_decide compiles the decision procedure to machine code and runs it, then asserts the result. It is fast, it is occasionally indispensable, and it adds the Lean compiler and the machine that ran it to the trusted base — a very large addition compared with the kernel. It announces itself in exactly one place:

'euler_polynomial_is_prime' depends on axioms: [Lean.ofReduceBool, propext, …]

Two problems, in order of severity. The proof is not kernel-checked, so “Lean verified it” is a weaker claim than it sounds. And the statement is still about a bounded family — the decide trap from item 9 — so even granting the computation, nothing has been established at $k = 40$ , where Euler’s polynomial gives $41^{2}$ and the pattern ends. A statement worth native_decide is usually a statement worth restating.

Both of these, and all seven audits above, come down to the same discipline. The compiler answers one question — does this proof prove this statement — and it answers it perfectly. Every other question is yours: what the statement says, what its words mean, whether anything satisfies it, and whether the theorem you have is the theorem you wanted. Part II is thirty theorems that have been through that process. Read them the same way.

Part one: reading Mathlib

Names are generated from statements

Reading a statement

open, and why a statement can mean different things in different files

Looking under the hood

Finding a lemma

Part two: the audit checklist

1. Are the hypotheses satisfiable?

2. Is the type right?

3. Where are the denominators?

4. Are the quantifiers in the right order?

5. Is a definition doing the theorem’s work?

6. What does the proof rest on?

7. Is decide proving a theorem or an instance?

The checklist

The audit exercise

Reading autoformalized Lean

`open`, and why a statement can mean different things in different files

7. Is `decide` proving a theorem or an instance?