Mathlib and autoformalization

This is the chapter the tutorial exists for.

You are unlikely to write much Lean. You are quite likely, over the next few years, to be handed some: a formalization of a lemma from your own paper, a “verified” appendix to somebody else’s, a proof produced by a model that also produced the statement it proves. In all three cases the thing you have to do is not write Lean but read it, and decide whether the theorem on the screen is the theorem you care about.

That decision has two halves. The first is vocabulary: almost every symbol in a real formal statement comes from Mathlib, and you cannot evaluate a statement whose words you cannot look up. The second is a checklist — a short list of mechanical checks that catch most of the ways a formalization goes wrong while still compiling. The compiler will confirm that a proof proves its statement. Nothing will confirm that the statement is the one you meant. That part is yours.

Everything here is quoted from lean/MrCLean/Fundamentals/Ch05Mathlib.lean, which CI compiles. Note that the “wrong” examples in the second half all compile, deliberately: that is the whole point of the exercise.

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 tabOpens with 62 lines of library preamble — the code above is at the bottom of the editor.

/- Mathlib names are generated from the *statement*, read left to right, with the
operations spelled out.  Once you know the vocabulary you can guess names, and —
more importantly — you can read a name and predict the statement.

* `mul_comm` : `a * b = b * a`.  Head symbol first, then the property.
* `add_div` : `(a + b) / c = a / c + b / c`.  The left-hand side is an addition
  inside a division; the name describes the LHS, not the RHS.
* `Finset.sum_add_distrib` : a sum of a sum distributes.  Namespaced by the type
  it is about.
* `Nat.cast_sub` : pushing the coercion `ℕ → ℝ` through a subtraction — and note
  the explicit hypothesis it needs.
* `sq_nonneg`, `sum_nonneg` : `0 ≤ …`.  `_nonneg`, `_pos`, `_ne_zero`, `_le`,
  `_lt` are the standard suffixes for order facts.
* `_of_` introduces a hypothesis (`Nat.sub_lt_of_lt`), `_iff` an equivalence
  (`sub_eq_zero_iff_eq`), `_eq_` a rewriting lemma. -/
#check @mul_comm
#check @add_div
#check @Finset.sum_add_distrib
#check @Nat.cast_sub
#check @sq_nonneg

/- Names also *drift*.  `div_add_div_same : a / c + b / c = (a + b) / c` was a
Mathlib lemma for years; today the same fact is `add_div`, stated in the other
direction.  This is why a snippet that compiled last year may not compile now,
and why `exact?` beats memory. -/

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 snippet 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 tabOpens with 88 lines of library preamble — the code above is at the bottom of the editor.

/- `#check @lemma` prints the statement with **every** argument explicit, which is
the only reliable way to see what a lemma really needs.  Read
`Finset.sum_le_sum` from the outside 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

* `{ι} {N}` — implicit types: the index (units) and the values (outcomes).
* `[AddCommMonoid N] [Preorder N] [AddLeftMono N]` — instance arguments, the
  mathematical setting.  `ℝ` has all three; so does `ℕ`.  This is where an
  autoformalized statement can quietly weaken itself.
* `{f g} {s}` — implicit, inferred from the goal.
* `(∀ i ∈ s, f i ≤ g i)` — the one explicit argument: the hypothesis you supply.
  Note its shape, `∀ i ∈ s`, not `∀ i`: this is the single most common source of
  "why does `exact h` fail". -/
#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 108 lines of library preamble — the code above is at the bottom of the editor.

/- `open Finset` lets you write `sum_add_distrib` for `Finset.sum_add_distrib` and
`#s` for `s.card`.  It changes nothing about the underlying names — but it does
change what a snippet needs in order to compile, which is why the preamble of
every chapter file says which namespaces are open. -/
#check @Finset.card_univ

/-- With `open Finset` in scope, `#z` is `z.card` and `card_univ` resolves. -/
theorem count_units (z : Assignment n) : (#z : ℝ) = (z.card : ℝ) := rfl

/-- Dot notation is namespace resolution in disguise: `P.tau` is
`Population.tau P`, found because `P : Population n`. -/
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.

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

/- Three commands for looking under the hood.

* `#print f` shows a definition's body — the fastest way to catch a definition
  that is not what its name claims.
* `#print axioms thm` lists everything the proof ultimately rests on.  A proof
  that used only ordinary mathematics reports exactly
  `[propext, Classical.choice, Quot.sound]`.
* `#check @thm` shows the statement with all arguments explicit. -/
#print Population.tau

/-- A completely ordinary theorem. -/
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
-- 'tau_of_no_effect' depends on axioms: [propext, Classical.choice, Quot.sound]

#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.

Finding a lemma

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

/-- Four ways to find a lemma, in the order worth trying.

1. `exact?` — searches for a single lemma closing the goal.  Slow, but it knows
   the whole library.  `apply?` is the version that accepts partial progress.
2. Guess the name from the conventions above and let autocompletion confirm it.
3. Loogle (<https://loogle.lean-lang.org>) searches by *shape*: typing
   `Finset.sum, _ * _` finds the lemmas relating sums and products.  Moogle
   searches by natural-language description.
4. The Mathlib docs (<https://leanprover-community.github.io/mathlib4_docs>),
   which are generated from the same source and always current.

The comment below is what `exact?` printed on this goal. -/
theorem sum_nonneg_example (v : Fin n → ℝ) : 0 ≤ ∑ i, (v i) ^ 2 := by
  -- `exact?` reports:  Try this: exact Finset.sum_nonneg fun i a => sq_nonneg (v i)
  exact Finset.sum_nonneg fun i _ => sq_nonneg (v i)

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, CI compiles it, and it appears on this page 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 tabOpens with 56 lines of library preamble — the code above is at the bottom of the editor.

/-- The difference-in-means estimator.  `#z` is the size of the treated set and
`zᶜ` is the control group; both denominators can be zero, which is the subject of
one of the audits below. -/
noncomputable def DiM (P : Population n) (z : Assignment n) : ℝ :=
  (∑ i ∈ z, P.y1 i) / (#z : ℝ) - (∑ i ∈ zᶜ, P.y0 i) / (#zᶜ : ℝ)

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 155 lines of library preamble — the code above is at the bottom of the editor.

/-- **Looks right, and is.**  The hypothesis `0 < n` is satisfiable — take
`n = 1` — and it is exactly the hypothesis the conclusion needs, because at
`n = 0` the mean is `0 / 0 = 0`. -/
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$ .

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.

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

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 163 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (warm-up).  **Vacuous hypotheses.**  The statement below asserts that
every population has zero average treatment effect.  It is provable, because
`0 < n₁ ∧ n₁ < 0` has no solutions in `ℕ`: from a contradiction, anything.

Prove it — `exfalso` then `omega`, which sees the contradiction in `h` — and then
never trust a hypothesis you have not checked is satisfiable.  The check itself
is a Lean statement: see `no_such_n₁` below. -/
theorem bad_vacuous (n₁ : ℕ) (h : 0 < n₁ ∧ n₁ < 0) (P : Population n) : P.tau = 0 := by
  sorry

/-- How to check satisfiability: try to *refute* the hypothesis set.  If you can,
the theorem above says nothing at all. -/
theorem no_such_n₁ : ¬ ∃ k : ℕ, 0 < k ∧ k < 0 := by
  rintro ⟨k, h1, h2⟩
  omega

Show solution

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

/-- Exercise (warm-up).  **Vacuous hypotheses.**  The statement below asserts that
every population has zero average treatment effect.  It is provable, because
`0 < n₁ ∧ n₁ < 0` has no solutions in `ℕ`: from a contradiction, anything.

Prove it — `exfalso` then `omega`, which sees the contradiction in `h` — and then
never trust a hypothesis you have not checked is satisfiable.  The check itself
is a Lean statement: see `no_such_n₁` below. -/
theorem bad_vacuous (n₁ : ℕ) (h : 0 < n₁ ∧ n₁ < 0) (P : Population n) : P.tau = 0 := by
  exfalso
  omega

/-- How to check satisfiability: try to *refute* the hypothesis set.  If you can,
the theorem above says nothing at all. -/
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 180 lines of library preamble — the code above is at the bottom of the editor.

/-- **Looks right, and is.**  Group sizes are naturals, but the arithmetic is done
in `ℝ` after an explicit cast, and `Nat.cast_sub` carries the `n₁ ≤ n` it needs. -/
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. Nat.cast_sub is the lemma that moves a ℕ subtraction across the cast, and — this is the part that matters — it requires k ≤ m. 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 — Nat.zero_le _ proves it — 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.

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 186 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (warm-up).  **The wrong type.**  Here is "no treatment ever harms
anybody", formalized over `ℕ`.  It is true — and it is true of *every* pair of
outcome vectors, including ones where treatment halves the outcome, because `ℕ`
subtraction truncates at zero: `3 - 5 = 0`.

Prove it (one lemma from the `Nat` namespace), then read the moral: if the
outcomes in an autoformalized statement live in `ℕ`, the statement is about
truncated arithmetic, not about your data. -/
theorem bad_nat_effect (y1 y0 : Fin 3 → ℕ) (i : Fin 3) : 0 ≤ y1 i - y0 i := by
  sorry

/- The truncation, made concrete. -/
#eval (3 : ℕ) - 5      -- 0
#eval (3 : ℤ) - 5      -- -2

Show solution

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

/-- Exercise (warm-up).  **The wrong type.**  Here is "no treatment ever harms
anybody", formalized over `ℕ`.  It is true — and it is true of *every* pair of
outcome vectors, including ones where treatment halves the outcome, because `ℕ`
subtraction truncates at zero: `3 - 5 = 0`.

Prove it (one lemma from the `Nat` namespace), then read the moral: if the
outcomes in an autoformalized statement live in `ℕ`, the statement is about
truncated arithmetic, not about your data. -/
theorem bad_nat_effect (y1 y0 : Fin 3 → ℕ) (i : Fin 3) : 0 ≤ y1 i - y0 i := by
  exact Nat.zero_le _

/- The truncation, made concrete. -/
#eval (3 : ℕ) - 5      -- 0
#eval (3 : ℤ) - 5      -- -2

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.

Right:

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

/-- **Looks right, and is.**  The treated-group mean, with the hypothesis that the
treated group is nonempty stated where it belongs. -/
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

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.

Prove it by unfolding DiM and letting simp only do the arithmetic; the lemma list is in the docstring, and the one that matters is div_zero.

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 208 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (core).  **Division by zero.**  Lean's `x / 0 = 0` is a convention,
and a "theorem" whose denominators can vanish may be true for that reason alone.

Below: the difference in means at the assignment that treats *nobody*.  It is
`0 - (average control outcome)`, and the `0` is not an estimate of anything — it
is `0 / 0`.  A design supported on `∅` would satisfy any number of
plausible-looking identities.

Prove it by unfolding `DiM` and simplifying: `Finset.sum_empty`,
`Finset.card_empty`, `Nat.cast_zero`, `div_zero`, `Finset.compl_empty`,
`Finset.card_univ`, `Fintype.card_fin`, `zero_sub`, `neg_div`. -/
theorem bad_div_zero (P : Population n) : DiM P ∅ = - (∑ i, P.y0 i) / n := by
  sorry

Show solution

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

/-- Exercise (core).  **Division by zero.**  Lean's `x / 0 = 0` is a convention,
and a "theorem" whose denominators can vanish may be true for that reason alone.

Below: the difference in means at the assignment that treats *nobody*.  It is
`0 - (average control outcome)`, and the `0` is not an estimate of anything — it
is `0 / 0`.  A design supported on `∅` would satisfy any number of
plausible-looking identities.

Prove it by unfolding `DiM` and simplifying: `Finset.sum_empty`,
`Finset.card_empty`, `Nat.cast_zero`, `div_zero`, `Finset.compl_empty`,
`Finset.card_univ`, `Fintype.card_fin`, `zero_sub`, `neg_div`. -/
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?

Right:

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

/-- **Looks right, and is.**  "However small a tolerance you name, some sample size
achieves it": `∀ ε, ∃ N`.  This is the statement an asymptotic claim makes. -/
theorem good_quantifier_order : ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, (1 : ℝ) / (N + 1) < ε :=
  fun _ hε => exists_nat_one_div_lt hε

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. 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)$ .

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

/-- Exercise (core).  **Quantifier order.**  Swap the two quantifiers and you get
"one sample size works for every tolerance", which is a different — and false —
claim.  Autoformalizers swap these routinely, and the swapped version often looks
tidier.

Prove that it is false: introduce the hypothetical `N` with `rintro ⟨N, h⟩`,
then feed the statement its own `ε = 1 / (N + 1)` (positive by `positivity`) and
watch it assert `1 / (N + 1) < 1 / (N + 1)`. -/
theorem bad_quantifier_order : ¬ ∃ N : ℕ, ∀ ε : ℝ, 0 < ε → (1 : ℝ) / (N + 1) < ε := by
  sorry

Show solution

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

/-- Exercise (core).  **Quantifier order.**  Swap the two quantifiers and you get
"one sample size works for every tolerance", which is a different — and false —
claim.  Autoformalizers swap these routinely, and the swapped version often looks
tidier.

Prove that it is false: introduce the hypothetical `N` with `rintro ⟨N, h⟩`,
then feed the statement its own `ε = 1 / (N + 1)` (positive by `positivity`) and
watch it assert `1 / (N + 1) < 1 / (N + 1)`. -/
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 241 lines of library preamble — the code above is at the bottom of the editor.

/-- **Looks right, and is.**  The estimand is defined from the potential outcomes
alone: it does not mention the assignment, so a theorem relating an estimator to
it has content. -/
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 rfl — 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 247 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (warm-up).  **A definition that bakes in the conclusion.**  Here the
"estimand" is defined to be the estimator.  "Unbiasedness" is then true by
definition — the proof is `rfl` — and says nothing whatsoever.

Prove it (one word), then note the two tells: the estimand takes the assignment
`z` as an argument, which no estimand should; and `#print` shows the body. -/
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

Show solution

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

/-- Exercise (warm-up).  **A definition that bakes in the conclusion.**  Here the
"estimand" is defined to be the estimator.  "Unbiasedness" is then true by
definition — the proof is `rfl` — and says nothing whatsoever.

Prove it (one word), then note the two tells: the estimand takes the assignment
`z` as an argument, which no estimand should; and `#print` shows the body. -/
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 261 lines of library preamble — the code above is at the bottom of the editor.

/-- **A `sorry` or an `axiom` hidden in a helper lemma.**  A theorem is only as
sound as everything it cites, and neither `sorry` nor `axiom` is visible at the
call site.  `#print axioms` is the check, and it is one line.

Compare.  A normal proof reports exactly the three standard axioms:

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

Now suppose a helper had been left unfinished:

```lean
theorem sorried (x : ℝ) : 0 ≤ x ^ 2 := by sorry
theorem uses_sorried (x : ℝ) : 0 ≤ x ^ 2 + 1 := by
  have := sorried x; linarith
#print axioms uses_sorried
```

which reports

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

`sorryAx` is the tell, and it propagates: any theorem citing `uses_sorried`
reports it too.  An `axiom` behaves the same way and is worse, because it is
silent — no warning is emitted at all:

```lean
axiom key_step (x : ℝ) : x ≤ x + 1
theorem helper (x : ℝ) : x - 1 ≤ x := by have := key_step (x - 1); linarith
#print axioms helper
-- 'helper' depends on axioms: [key_step, propext, Classical.choice, Quot.sound]
```

Run `#print axioms` on the headline theorem of anything you did not write. -/
theorem clean_proof (x : ℝ) : 0 ≤ x ^ 2 + 1 := by positivity

#print axioms clean_proof
-- 'clean_proof' depends on axioms: [propext, Classical.choice, Quot.sound]

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
-- 'helper' depends on axioms: [key_step, propext, Classical.choice, Quot.sound]

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 303 lines of library preamble — the code above is at the bottom of the editor.

/-- **Looks right, and is.**  `decide` is legitimate when the claim really is a
finite check: here, over the three units of a three-unit study. -/
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 by decide for $k < 3$ . The check succeeds, and the claim is false at $k = 3$ : $9 > 8$ . Both halves are one tactic.

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 307 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (core).  **`decide` on the small instance.**  "There are at least as
many possible assignments as ordered pairs of units", i.e. `k ^ 2 ≤ 2 ^ k`,
checked by `decide` for `k < 3`.  The check succeeds.  The claim is false at
`k = 3`: `9 > 8`.

Prove both — each is one tactic — and then treat every `decide` in an
autoformalized proof as a claim about the instances it enumerated and nothing
more. -/
theorem bad_decide_small : ∀ k < 3, k ^ 2 ≤ 2 ^ k := by
  sorry

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

Show solution

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

/-- Exercise (core).  **`decide` on the small instance.**  "There are at least as
many possible assignments as ordered pairs of units", i.e. `k ^ 2 ≤ 2 ^ k`,
checked by `decide` for `k < 3`.  The check succeeds.  The claim is false at
`k = 3`: `9 > 8`.

Prove both — each is one tactic — and then treat every `decide` in an
autoformalized proof as a claim about the instances it enumerated and nothing
more. -/
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 321 lines of library preamble — the code above is at the bottom of the editor.

/-- **The checklist**, in the order that catches the most for the least effort.

1. **Read the conclusion alone.**  Is it the statement you wanted, with nothing
   extra quantified and nothing missing?
2. **Are the hypotheses satisfiable?**  Try to refute them.  A contradictory
   hypothesis set proves everything.
3. **Is any hypothesis unused?**  Lean's linter says so ("Variable name `h` is
   not explicitly referenced").  An unused hypothesis means the theorem is
   stronger than advertised — or that the work is being done somewhere you have
   not looked.
4. **Check the types.**  `ℕ` subtraction truncates, `ℕ` division floors.  Sample
   sizes may be `ℕ`; outcomes and estimates must be `ℝ`.
5. **Find the denominators.**  `x / 0 = 0`, so any claim about a ratio is
   trivially true where the denominator vanishes.
6. **Check quantifier order.**  `∀ ε, ∃ N` and `∃ N, ∀ ε` are different claims.
7. **`#print` every definition the statement mentions.**  A definition that
   already contains the conclusion turns the theorem into `rfl`.
8. **`#print axioms` the theorem.**  Anything beyond
   `[propext, Classical.choice, Quot.sound]` — especially `sorryAx` — voids it.
9. **Distrust `decide` and `norm_num` on parametrised claims.**  They verify
   instances, not theorems. -/
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.

The shape: for each z, by_cases on whether D.prob z = 0. In the zero branch both sides of the summand are 0 * _. Off the null set, hbal rewrites DiM P z to P.tau. That turns the sum into ∑ z, D.prob z * P.tau, which is ← Finset.sum_mul and then D.sum_one.

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

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

/-- Exercise (core).  **Audit this.**  Asked to formalize "under a design that
assigns a fixed number of units to treatment, the difference in means is unbiased
for the average treatment effect", a language model produced the statement below,
with a proof.

It compiles.  Prove it yourself — the proof is short, and writing it is how you
find the flaw — and then say what is wrong with it as a formalization of
unbiasedness.

Hint for the proof: split each term of `D.expect (DiM P)` by `by_cases` on
`D.prob z = 0`, rewrite with `hbal` off the null set, then `← Finset.sum_mul`
and `D.sum_one`. -/
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

Show solution

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

/-- Exercise (core).  **Audit this.**  Asked to formalize "under a design that
assigns a fixed number of units to treatment, the difference in means is unbiased
for the average treatment effect", a language model produced the statement below,
with a proof.

It compiles.  Prove it yourself — the proof is short, and writing it is how you
find the flaw — and then say what is wrong with it as a formalization of
unbiasedness.

Hint for the proof: split each term of `D.expect (DiM P)` by `by_cases` on
`D.prob z = 0`, rewrite with `hbal` off the null set, then `← Finset.sum_mul`
and `D.sum_one`. -/
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. Reuse the argument you just wrote, with (DiM P z - P.tau) ^ 2 in place of DiM P z; the zero-variance conclusion follows from Finset.sum_const and smul_zero.

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

/-- Exercise (stretch).  **The flaw, and how to see it.**

`hbal` says the estimator equals the estimand on *every assignment the design can
produce*.  That is not unbiasedness; it is exactness.  Unbiasedness is a
statement about an average — `DiM` is allowed to be wrong on every single
assignment, provided the errors cancel — and it is the whole content of the
theorem.  Here the content has been moved into a hypothesis, and what remains is
linearity of expectation.

Three tells, all mechanical:

* the hypothesis mentions the estimator `DiM` and the estimand `tau` together,
  which a *hypothesis about the design* has no business doing;
* the design is arbitrary: `n₁`, complete randomisation and the support condition
  the informal statement mentions never appear;
* `hbal` is unsatisfiable for any interesting population — which the exercise
  below proves.

Prove that `hbal` forces the estimator to have zero variance: under it, `DiM` is
constant on the support, so `E[(DiM - τ)²] = 0`.  Reuse the argument you just
wrote, with `(DiM P z - P.tau) ^ 2` in place of `DiM P z`. -/
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

Show solution

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

/-- Exercise (stretch).  **The flaw, and how to see it.**

`hbal` says the estimator equals the estimand on *every assignment the design can
produce*.  That is not unbiasedness; it is exactness.  Unbiasedness is a
statement about an average — `DiM` is allowed to be wrong on every single
assignment, provided the errors cancel — and it is the whole content of the
theorem.  Here the content has been moved into a hypothesis, and what remains is
linearity of expectation.

Three tells, all mechanical:

* the hypothesis mentions the estimator `DiM` and the estimand `tau` together,
  which a *hypothesis about the design* has no business doing;
* the design is arbitrary: `n₁`, complete randomisation and the support condition
  the informal statement mentions never appear;
* `hbal` is unsatisfiable for any interesting population — which the exercise
  below proves.

Prove that `hbal` forces the estimator to have zero variance: under it, `DiM` is
constant on the support, so `E[(DiM - τ)²] = 0`.  Reuse the argument you just
wrote, with `(DiM P z - P.tau) ^ 2` in place of `DiM P z`. -/
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

-- WRONG: read the `open`, not the statement
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

-- WRONG: not what the kernel checked
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?