How to read a statement — when you are handed "checked in Lean"

When you receive a result described as "checked in Lean", there are seven things you can confirm. The first four are left to the machine and are over in a few minutes. The last three are for you to read, and they are the substance.

The order matters. The first half looks at "is the proof really closed?", the second half at "is the closed statement the problem you were asking about?". It is quite normal for the first half to pass and the second half not to, and the four types this takes are listed in 08.

Unpack the bundle and run the check through on your own machine. The Lean verification bundle comes with verify.sh, which sets the parallelism from the machine's RAM and CPU count, runs lake exe cache get and the whole build in one go, and finally summarises the list of axioms and the number of holes. Unpack and run that one script; that is all.

When you want to look at one particular file, the fastest way is to hand a self-contained single file (the concatenated version), which depends on no other file, straight to lake env lean. The concatenated version reads nothing but the one line import Mathlib, so that single file is known to close on its own.

$ time lake env lean PerfectFamily.lean
'PerfectFamily.cube3_bool' does not depend on any axioms
'PerfectFamily.dir_count' depends on axioms: [propext, Quot.sound]
   ...(22 more lines: the `#print axioms` output looked at in ③)
real	0m7.367s
$ echo $?
0

The exit code is not the only thing to look at. Lean can emit warnings even when there are no errors, and among the warnings are things that matter in later steps (a use of sorry, a deprecated name). Confirm that there is not a single line of error or warning. In the run above, what appears is only the output of #print axioms; errors and warnings were 0 lines, and the exit code was 0.

If the check does not pass, suspect the environment first. The versions of Lean and mathlib are pinned by the bundle's lean-toolchain and lake-manifest.json, so if the versions match, the results agree. The ways a version mismatch makes things fail are collected at the end of 11 Common pitfalls.

Lean has ways of writing "put the proof off until later", and a theorem that uses them still passes the check. Search the whole source mechanically.

grep -rn -E 'sorry|admit|native_decide|nativeDecide|ofReduceBool' .

A theorem that uses sorry also shows up as a warning. Put one in as a trial and check, and this comes out.

warning: declaration uses `sorry`

This warning is a single line, and in a long output it gets overlooked. The grep of ② and the axiom check of ④ exist to look at the same thing from another side.

#print axioms theorem-name lists what the theorem ultimately depends on. It is the result of following the whole dependency tree, so a hole anywhere along the way necessarily shows up.

#print axioms PerfectFamily.no_perfectZ_of_five

The output looks like this.

'PerfectFamily.no_perfectZ_of_five' depends on axioms: [propext, Quot.sound]

There is a single standard for reading it.

A clean axiom column guarantees nothing about the statement meaning anything. A theorem with a false hypothesis, or a universal statement over the empty set, passes within the three standard axioms (real examples in 08 §04). This step looks only at "is the proof closed?".

When there are several headline theorems, keep one file that is nothing but a list of #print axioms, and every check will print all the axioms. In the bundle, ChkAll.lean plays that role.

From here on is the substance. Do not read the theorem's name; read the statement. Then open every definition that appears in the statement, one by one, and match it against the definition on paper.

As an example, take a theorem about families of edges of the hypercube. The statement is this.

theorem no_perfectZ_of_five {d : ℕ} (hd : 5 ≤ d) (J : Fin d → W d → Bool) : ¬ PerfectZ J

What can be read off is only "for d ≥ 5, PerfectZ is satisfied by no J". Without knowing what PerfectZ is, this theorem says nothing. Open it.

/--
`J μ x`: the edge from `x` towards `x + e_μ` is in the family.

`PerfectZ J`: for every plaquette `(μ, ν, x)` (`μ ≠ ν`), exactly one of its 4 edges
`(μ, x)`, `(μ, x+e_ν)`, `(ν, x)`, `(ν, x+e_μ)` is in `J`.
-/
def PerfectZ (J : Fin d → W d → Bool) : Prop :=
  ∀ μ ν : Fin d, μ ≠ ν → ∀ x : W d,
    (J μ x).toNat + (J μ (shift x ν)).toNat
      + (J ν x).toNat + (J ν (shift x μ)).toNat = 1

What has to be matched here is whether "the 4 edges of the plaquette" are the same 4 edges as on paper. Look at the four terms one at a time. shift x ν is a definition not yet opened, so open that too.

def shift (x : W d) (i : Fin d) : W d := Function.update x i (x i + 1)

It is the function that takes x and increases only its i-th coordinate by 1. So the four terms are: out of x, the edge in direction μ; out of x + e_ν, the edge in direction μ; out of x, the edge in direction ν; and out of x + e_μ, the edge in direction ν — these are the 4 edges of the square in the plane (μ, ν). It agrees with the definition on paper.

Look inside W d as well.

/-- The vertices of `ℤ^d`. -/
abbrev W (d : ℕ) : Type := Fin d → ℤ

It is the infinite lattice. No period is imposed, so the theorem includes families that are not periodic. This is a point that bears directly on the strength of the statement, and you cannot see it without looking at the type. There is a separate theorem stating the same "perfect family" on the periodic lattice Fin d → ZMod L, and that one and this one are different theorems.

This sequence is the procedure.

Following this procedure is what turns up the type in 08 §02, "two definitions under the same word". Even when the names of the definitions are the same, if what you find inside them differs, they are different theorems.

What is lined up to the left of the : in the statement are the hypotheses. For each one, decide who satisfies it.

The third kind is the crux. Pushing the awkward part out into a hypothesis and closing the rest is a normal way to proceed, but if nobody satisfies the hypothesis that was pushed out, the conclusion cannot be used yet. 08 §05 has a real instance where the hypotheses go away across three stages of theorems stating the same conclusion.

There is one way to tell. Is there, in the same bundle, a theorem giving a concrete example that satisfies that hypothesis? If there is, the push-out has been resolved; if not, it has not.

A decision that returned "it holds" under decide may be a decision that simply lets everything through. Controls are what rule this out.

For a negative control, look for whether something that breaks the correct answer in just one place is included. If only the empty one and the full one fail, a coarse decision procedure would still pass. Real examples are in 08 §04 (b).

If there is not a single control, that does not mean the result is wrong, but the receiving end will have to write its own controls and confirm. It is only a matter of feeding extreme inputs to the decision function and running decide, so a few lines will do.

A body of results ought to come with a table saying which grade each row is. When there is no table, the following three have been handed over mixed together.

Leanmachine-checked. Look for a theorem name attached. A row with no name gives you no means of confirming it. papera proof exists but has not been machine-checked. Look for a statement of how far the paper part reaches. computationthe range confirmed by computation on that machine. Look for it not having been made into a claim for the outside.

The point when looking at the table is to find the seam between the Lean rows and the paper rows. If the seam is right before the conclusion, the conclusion is of paper grade. 08 §06 has two examples, both written so that the seam is visible in one place.

One more thing: look for whether the row "the enumeration is exhaustive" is in the table. In a result that lines up candidates and knocks them down one by one, the candidates lined up being all of them is a separate grade. This row is easily dropped, and when it is, the whole upper bound looks machine-checked (10 §03).

The commonest shape is that 1–4 pass and somewhere in 5–8 does not. The result is then not wrong; rather, the statement is not what you thought it was. The type of the difference falls under one of the four in 08.

Next: 10 When Lean is too heavy — the background for reading, on the receiving end, "why is this row still paper?". Terms are in the 12 Glossary.