Does it say what you meant? — passing the check, and having written the problem

When Lean says "it checks", all it is saying is that the statement you wrote follows from the proof you wrote. Whether the statement you wrote is the problem you wanted to solve, Lean does not look at. Change one character in a definition and you have a different claim, and the proof may still go through.

There are four types that keep recurring in how things fall into this gap. For each type, a small example that was actually checked and passed is paired with a real instance that turned up among the machine-checked results.

All the Lean code on this page, the examples that pass and the ones that fail alike, was checked locally, with Lean 4 (v4.33.1) and mathlib.

A small example — dropping "at least 2" from the definition of a prime

A prime is sometimes explained as "a number with no divisors other than 1 and itself". Write that into Lean just as it stands. The upper bound ∀ m ≤ n is there to make the decision finite so that it can be put on decide; for n ≥ 1 every divisor is at most n anyway, so the condition is unchanged.

def MyPrime (n : ℕ) : Prop := ∀ m ≤ n, m ∣ n → m = 1 ∨ m = n

Put 1 into this definition. The only divisor of 1 is 1, and that counts as "1 or n", so the condition is satisfied.

theorem myPrime_one : MyPrime 1 := by decide
theorem not_prime_one : ¬ Nat.Prime 1 := by decide

Both lines pass. So MyPrime is a different predicate from mathlib's Nat.Prime. At 7 the two give the same answer, so trying a few values would not reveal it.

theorem both_seven : MyPrime 7 ∧ Nat.Prime 7 := by decide

The fix is to add 2 ≤ n. And after the fix, have Lean confirm over a finite range that the corrected definition agrees with the definition that already exists.

theorem fixed_agrees : ∀ n ≤ 20, ((2 ≤ n ∧ MyPrime n) ↔ Nat.Prime n) := by decide

The last line is what does the work. Agreement up to 20 is not a proof, but a slip in the writing is caught here. It is a good habit to attach to any newly written definition a line that checks, over a finite range, that it agrees with the one already there.

A real instance — "can be placed", for a unit-distance graph, has a weak version and a strong version

A unit-distance graph has distinct points in the plane as its vertices, and two points joined by an edge are at distance exactly 1. The question is whether a given graph can be placed in the plane in that form. When this "can be placed" is written in Lean, two definitions come out.

The weak version demands only that two points joined by an edge are at distance 1, and says nothing about the distance between two points not joined by an edge. This is the form used in how the certificates are built.

/-- Edge condition only (nothing imposed on non-edges, no injectivity either). -/
def Edges (E : List (ℕ × ℕ)) (x y : ℕ → ℝ) : Prop :=
  ∀ e ∈ E, (x e.1 - x e.2)^2 + (y e.1 - y e.2)^2 = 1

The strong version demands both directions: edge ⟺ distance 1. Two points not joined by an edge must not be at distance 1. The two go by the same name, yet they are different predicates. A small picture brings out the difference.

/-- Squared distance (realisations are written with squares, to avoid square roots). -/
def sq2 (a b : ℝ × ℝ) : ℝ := (a.1 - b.1) ^ 2 + (a.2 - b.2) ^ 2

/-- **Weak version**: two points joined by an edge are at distance 1. Nothing imposed on non-edges. -/
def WeakReal (E : List (ℕ × ℕ)) (p : ℕ → ℝ × ℝ) : Prop :=
  ∀ e ∈ E, sq2 (p e.1) (p e.2) = 1

/-- **Strong version**: over the range of `n` points, edge ⟺ distance 1. -/
def FaithReal (n : ℕ) (E : List (ℕ × ℕ)) (p : ℕ → ℝ × ℝ) : Prop :=
  ∀ i < n, ∀ j < n, i ≠ j → ((((i, j) ∈ E) ∨ ((j, i) ∈ E)) ↔ sq2 (p i) (p j) = 1)

Take the graph whose edges are just the 6 spokes from the centre, with the perimeter of the regular hexagon not made into edges. For the picture, use the ordinary arrangement: the centre and the unit regular hexagon around it (s is √3 / 2).

def hexE : List (ℕ × ℕ) := [(0, 1), (0, 2), (0, 3), (0, 4), (0, 5), (0, 6)]

noncomputable def hexP : ℕ → ℝ × ℝ
  | 1 => (1, 0)
  | 2 => (1 / 2, s)
  | 3 => (-(1 / 2), s)
  | 4 => (-1, 0)
  | 5 => (-(1 / 2), -s)
  | 6 => (1 / 2, -s)
  | _ => (0, 0)

This picture satisfies the weak version but not the strong version, because two adjacent points on the perimeter are at distance 1 without being joined by an edge.

theorem hex_weak : WeakReal hexE hexP
theorem hex_not_faith : ¬ FaithReal 7 hexE hexP

There is only one direction connecting the two definitions. If it can be placed in the strong sense, it can be placed in the weak sense. The converse fails, as the example above shows.

theorem weak_of_faith (n : ℕ) (E : List (ℕ × ℕ))
    (hE : ∀ e ∈ E, e.1 < n ∧ e.2 < n ∧ e.1 ≠ e.2) (p : ℕ → ℝ × ℝ)
    (h : FaithReal n E p) : WeakReal E p

theorem no_faith_of_no_weak (n : ℕ) (E : List (ℕ × ℕ))
    (hE : ∀ e ∈ E, e.1 < n ∧ e.2 < n ∧ e.1 ≠ e.2)
    (h : ∀ p : ℕ → ℝ × ℝ, ¬ WeakReal E p) :
    ∀ p : ℕ → ℝ × ℝ, ¬ FaithReal n E p

From here, which definition to use is decided by what you want to say.

Under the single word "realisation" sit two definitions, and one bridge between them is needed. This only became visible once it was written in Lean; on paper, the single phrase "can be placed" had gone by unnoticed. On the machine-checked side, the certificates of non-placeability are written in the weak version (Edges, Realiz), while the parts used in the upper-bound argument assume the strong version. For now the two are separate theorems, and the bridge has not been built.

A small example — "everything in the list satisfies the condition" versus "everything satisfying the condition is in the list"

Make a list of three primes and prove that all of them are prime. Count the length of the list as well.

def cand : List ℕ := [2, 3, 5]

theorem cand_all_prime : ∀ n ∈ cand, Nat.Prime n := by decide
theorem cand_card : cand.length = 3 := by decide

Both lines pass. But neither of them says "the primes are exhausted by this list". 7 is missing.

theorem cand_not_complete : ¬ (∀ n, Nat.Prime n → n ∈ cand) := by
  intro h
  have h7 := h 7 (by decide)
  revert h7
  decide

This passes too. That is, cand_all_prime and cand_card, together with cand_not_complete, hold at the same time. The mistake is to look at the first two and read "all the primes are covered".

A real instance — "none of the 117 classes can be placed" is not "the candidates are exactly these 117 classes"

On the unit-distance-graph side there is a statement of the same shape. The candidates on 11 vertices with independence number at most 3 are enumerated, and the theorem proves, for each one of them, that it cannot be placed in the plane.

theorem hn11_no_realiz : ∀ E ∈ cands, ∀ p : Fin 11 → ℝ × ℝ, ¬ Realiz E p
theorem cands_card : cands.length = 117 := by decide

What these two say is that none of the 117 edge sets listed in cands can be placed in the plane at unit distance, and that cands has length 117. "The graphs on 11 vertices with independence number at most 3 are exhausted by the 117 classes in cands" — the completeness of the enumeration is nowhere in these two lines. Completeness was confirmed by a computation outside Lean, and its grade is computation.

Short theorem names are easier to read, but a short name invites a reading broader than the statement. From the name hn11_no_realiz one can read "the 11-vertex case is settled". You have to read the statement, not the name, and the procedure for that is written out in 09 How to read a statement.

A small example — if the hypothesis is false, any conclusion will do

A theorem with a false hypothesis passes whatever you write as its conclusion.

theorem foo (h : 2 + 2 = 5) : 0 = 1 := by omega

"For every element" over the empty set also passes without the content being looked at.

theorem bar : ∀ x ∈ (∅ : Finset ℕ), x = x + 1 := by decide

Apply #print axioms (the command that lists the axioms a theorem depends on) to these two, and this comes out.

'G08.foo' depends on axioms: [propext, Quot.sound]
'G08.bar' depends on axioms: [propext, Classical.choice, Quot.sound]

Both are within the three standard axioms, and no sorryAx (an unproved hole) appears either. A clean axiom column guarantees nothing about the statement being non-vacuous. foo shows only two axioms and looks "cleaner" than a theorem showing three, but there is nothing inside it.

The countermeasure — put a non-emptiness check and a negative control inside Lean

Being vacuously true is not in itself an error. It becomes one when you read "it holds" without noticing that it is vacuous. On the machine-checked side, countermeasures are in place in the following three forms.

/-- The hypotheses are satisfied at `L = 4` (the theorem is not empty). -/
example (x : V 4) (μ ν : Fin 4) (h : μ ≠ ν) :
    ∃! e : Edge 4, InP e x μ ν ∧ Istar (L := 4) ⟨2, rfl⟩ e :=
  plaq_unique _ x μ ν h

example (e : Rest (L := 4) ⟨2, rfl⟩) :
    (Finset.univ.filter (fun s => e ∈ Es (L := 4) ⟨2, rfl⟩ s)).card = 6 :=
  star_count _ (two_ne_zero_of_le (by norm_num)) e

/-- The edge from the origin in direction 3 is in `I*` (`x₁ = x₂ = x₄`): the family of stars is non-empty. -/
example : Istar (L := 4) ⟨2, rfl⟩ ((0 : V 4), (2 : Fin 4)) := by
  unfold Istar red
  simp only [Pi.zero_apply, map_zero]
  decide

The last one says "the family itself is non-empty". If the family were empty, "every edge of the family ..." would be vacuously true.

/-- Negative control: the empty family is not perfect (`d = 3`). -/
theorem not_perfect_empty3 : ¬ Perfect (fun (_ : Fin 3) (_ : V 3) => false) := by decide

/-- Negative control: the family of all edges is not perfect (`d = 3`). -/
theorem not_perfect_full3 : ¬ Perfect (fun (_ : Fin 3) (_ : V 3) => true) := by decide

/-- Negative control: replacing direction 0 of `I4` by everything makes it not perfect (`d = 4`). -/
theorem not_perfect_I4_broken :
    ¬ Perfect (fun (μ : Fin 4) (x : V 4) => if μ = 0 then true else I4 μ x) := by decide

The third is what does the work. Put in a family that breaks the correct answer in just one place, and see the decision fail. If only the empty family and the full family fail, a coarse decision procedure would still pass.

The same file also has a line that, conversely, states as a theorem that something is vacuously true.

/-- For `d ≤ 1` there are no 2-dimensional faces, so every family is perfect (vacuously true). -/
theorem perfect_of_le_one {d : ℕ} (hd : d ≤ 1) (I : Fin d → V d → Bool) : Perfect I

This is not the discovery that "there are perfect families even for d ≤ 1"; it is the warning that in those dimensions the statement has no content. Give the vacuous range a name and bracket it off, and the conclusion will not be misread.

structure IsHaarS3 (μ : Measure ℍ[ℝ]) : Prop where
  prob : IsProbabilityMeasure μ
  unit : ∀ᵐ u ∂μ, ‖u‖ = 1
  inv : ∀ q : ℍ[ℝ], ‖q‖ = 1 → μ.map (fun u => q * u) = μ

These three conditions (total mass 1; almost every point has norm 1; invariant under multiplication on the left by an element of unit norm) pin down "the uniform measure on the 3-sphere". There is a theorem that builds a measure satisfying them concretely and shows that it does.

theorem isHaarS3_haarS3 : IsHaarS3 haarS3

haarS3 is Lebesgue measure restricted to the unit ball, pushed forward by x ↦ x/‖x‖, and normalised to total mass 1. Because this one line exists, no theorem that assumes IsHaarS3 μ is vacuous. Once you define something by its properties, build one concrete object that has them — the two go as a pair.

When a large claim is put into Lean, it is common to push the awkward part out into a hypothesis first and close only the rest. The theorem then exists "with hypotheses attached". Until someone satisfies the hypothesis, the conclusion cannot be quoted on its own.

A real instance — until "every edge lies in exactly 6 stars" leaves the hypotheses

There is a theorem giving a lower bound on the second derivative of the effective action in lattice gauge theory. In its first form it was an abstract statement with the whole geometry of the lattice pushed out into hypotheses. h6 is the centre of it: it takes the lattice property "every edge lies in exactly 6 stars" as a hypothesis, without proving it.

theorem hess_star_family {S E : Type*} [Fintype S] [Fintype E] [DecidableEq E]
    (Es : S → Finset E) (h6 : ∀ e, (univ.filter (fun s => e ∈ Es s)).card = 6)
    (x : E → ℝ) (hx : ∀ e, 0 ≤ x e) (β : ℝ)
    (q A B C : S → Fin 6 → ℍ[ℝ]) (hq : ∀ s i, ‖q s i‖ = 1)
    (hA : ∀ s i, (A s i).re = 0) (hB : ∀ s i, (B s i).re = 0) (hC : ∀ s i, (C s i).re = 0)
    (hslot : ∀ s, ∑ i, (‖A s i‖ ^ 2 + ‖B s i‖ ^ 2 + ‖C s i‖ ^ 2) ≤ ∑ e ∈ Es s, x e) :
    -(27 * β ^ 2) * ∑ e, x e ≤
      deriv (deriv (fun τ => ∑ s, -G β (‖∑ i, curve (q s i) (A s i) (B s i) (C s i) τ‖ ^ 2))) 0

Nine hypotheses are lined up. To say at this stage that "the lower bound on the second derivative is closed in Lean" would be to hand over the conclusion without saying whether any lattice satisfies the nine hypotheses.

In the next stage a theorem came in showing that h6 really does hold for a concrete lattice.

theorem star_count (hL : (2 : ZMod L) ≠ 0) (e : Rest h2) :
    (univ.filter (fun s => e ∈ Es h2 s)).card = 6

In the stage after that, the perturbation was rewritten in the language of the lattice, and the remaining hypotheses went away too. In the final form the hypotheses are only the type of the field and the condition on the period.

theorem hess_gauge [NeZero L] (h2 : 2 ∣ L) (hL : 3 ≤ L) (U X : Rest h2 → ℍ[ℝ])
    (hU : ∀ e, ‖U e‖ = 1) (hX : ∀ e, (X e).re = 0) (β : ℝ) :
    -(27 * β ^ 2) * ∑ e, ‖X e‖ ^ 2 ≤
      deriv (deriv (fun τ => Phi h2 (two_ne_zero_of_le hL) β (pert h2 U X τ))) 0

2 ∣ L (the period is even), 3 ≤ L, ‖U e‖ = 1 (the field is a unit quaternion), (X e).re = 0 (the generator of the perturbation is purely imaginary). These four are exactly what "being a configuration of lattice gauge theory" means; they are not hypotheses that were pushed out.

When you say "closed in Lean", say the list of hypotheses along with it. All three stages state "a lower bound on the second derivative", but the range in which a reader can use them is entirely different.

There is one countermeasure common to all four types. For a body of results, make a table of "how far is Lean, from where is it paper, and which part is computation", and put it alongside the results. The work of making the table is itself what flushes out the four types above.

The labels mean the same across the site.

Leanmachine-checked (at most the three standard axioms, no sorryAx, theorem name attached) papera proof exists but has not been machine-checked computationthe range confirmed on this machine; not made into a claim for the outside knowna restatement, a known theorem, or a check against the outside literature

Example 1 — the unit-distance-graph side

Looking at the first three rows alone, both the upper and the lower bound appear machine-checked, but the upper bound needs the fourth row. Once it is in a table, the row that is needed and missing is visible to the eye.

Example 2 — the lattice-gauge-theory side

What follows concerns a constant in the strong-coupling regime; there is no claim about the continuum limit or the body of the mass-gap problem.

In this table, the seam between the Lean rows and the paper rows is visible in one place — where the lower bound on the second derivative (Lean) hands over to the lower bound on curvature (paper). Write the seam without hiding it, and the reader can inspect that spot for themselves.

Next: 09 How to read a statement — the four types on this page, turned into a checklist for whoever receives a result. Terms are in the 12 Glossary.