2026-10-01 · chapter Yang–Mills and the mass gapAppendicesLean and machine checking

Lean and machine checking — what the label "Lean" guarantees is only the arrow from premises to conclusion

Sentences in this book carry five kinds of label (the legend in 0-01): Lean, Paper, Computed, Known and Physics. Of these, the Lean label looks the strongest and is the most easily misread.

The typical misreading is to read "checked in Lean" as "settled as true". What Lean confirms is that the written conclusion follows logically from the written premises. Whether the premises hold, and whether the statement says the intended mathematics, lie outside Lean. This appendix shows that boundary with small examples that were actually checked.

Written as a formula, a sentence with the Lean label has the following form.

What the label guarantees is the arrow in the middle. If the premises $P_i$ contain unproved assumptions (for example 10-01 The line of construction and Assumption H) or measured numbers, the conclusion $Q$ is conditional to the same extent. When this book cites a Lean theorem name, it writes the premises on the same line.

$C_P$ (the Poincaré constant, Part 10), $m$ (the mass) and $\xi$ (the correlation length) are quantities of Part 10, but in this appendix it is enough to read them as plain real numbers.

Example. "If $m \gt 0$, $C_P = 1/m^2$ and $C_P \le K\xi^2$, then $1 \le K(m\xi)^2$" is a statement that only multiplies both sides by $m^2$, and it can be confirmed in Lean (in §03 this machine actually checks it). But whether $C_P \le K\xi^2$ holds in four-dimensional Yang–Mills theory has nothing to do with this arrow. That is an assumption.

The division of work between this appendix and this site's guide to Lean (thirteen pages) is as follows. The guide is an introduction to Lean itself, covering installation, how to assemble concrete proofs, and common pitfalls. This appendix restricts itself to the minimum needed to read this book, and to how this book decides its labels. The correspondence of each theorem's premises with the known results is listed in 10-13.

Lean is both a programming language and a tool for checking proofs. It can do both with one mechanism because it treats propositions as types, and proofs as values (terms) of those types.

In a program we write "3 is a value of the type of natural numbers Nat". In Lean, with the same notation, we write "p is a proof of the proposition $P$".

The formula on the right is read "$p$ has type $P$", and that means "$p$ is a proof of $P$". Type checking can be done mechanically, so checking proofs becomes mechanical too.

A proposition with premises becomes a function type. A proof of "if $P_1$ and $P_2$ then $Q$" is a function that takes a proof of $P_1$ and a proof of $P_2$ and returns a proof of $Q$.

This is what the arrow of formula (1) really is. In the declaration of a Lean theorem, the arguments lined up to the left of the colon (brackets like (hm : 0 < m)) are the premises, and the right of the colon is the conclusion. When reading, the most important thing is this row of brackets ("Make a list of the hypotheses" in the guide).

Example. The smallest example checked on this machine is the following one line.

theorem pos_nat (n : Nat) (h : 0 < n) : 0 < n := h

The premise h is itself the proof of the conclusion. It is a theorem with no content, but the form "a function that takes a premise and returns a conclusion" is clearly visible.

The other pillar is the kernel. The proof a person writes is a script lined up from tactics (commands that direct one step of a proof; §03), and Lean expands it into a term of the form of formula (2). Finally that term is type-checked by the kernel, a checker kept small. Even if a tactic has an error, a term the kernel does not pass does not become a theorem. Narrowing what is trusted down to the one kernel is where the trust in machine checking comes from ("Kernel and tactics" in the guide, How checking works).

Detour: the name of the correspondence between propositions and types

When writing a proof in Lean, "what must be shown now" is always on the screen. This is called the goal. The goal is written to the right of the symbol $\vdash$, and the hypotheses that may be used are lined up above it. Each time one tactic is entered, a hypothesis or the goal is rewritten, and when no goals remain the proof is finished.

As an example we use the statement of §01 written in Lean. There are three premises (excluding the types of the variables). It is the same statement as hup_is_gap_positivity in 10-13, with only the names of the variables different.

On paper it is three lines: "substitute $C_P$, multiply both sides by $m^2 \gt 0$, and tidy up". In Lean it takes four steps, and the second step, have, is preparation for multiplying by $m^2$. The correspondence is: substitution is step 1, multiplication is steps 2 and 3, tidying is step 4. In Lean, what each step rewrote is recorded mechanically. The numbers in Figure 1 (the text of the goals) are copied as they are from the states that Lean 4.33.1 on this machine output in the middle of the proof.

ComputedThe numbers in this figure were computed on this machine (checked with Lean 4.33.1 with trace_state inserted after each step, and the output copied as it is; the figure omits the trace_state lines. The "No goals" of step 4 is not a copy of output; it was confirmed by finishing without errors). On a narrow screen the same content can be read in Table 1.

Table 1 has the same content as Figure 1.

How to read it. At step 3, hH has almost the same form as the goal; the only difference is the order of the product. The final ring confirms that reordering as an identity. You can see that the three lines on paper correspond to Lean's four steps with just one preparatory step added. Detailed examples of choosing steps in Lean are in "The skeleton of the proof" in the guide.

What Lean confirmed in this example is only algebra. Inside Lean, $C_P$ is just a named real number, and that it is a Poincaré constant is not checked. We look at this point for the theorems of the whole book in §06.

Lean provides two ways of skipping part of a proof. One is sorry, a mark meaning "fill this in later". The other is an axiom, a statement declared true without proof. With either, the theorem passes. So the fact that it "passed" alone does not tell you there are no holes.

The tool for finding holes is #print axioms. Given a theorem name, it lists which axioms that theorem ultimately depends on (following the statement and the proof). sorry is internally replaced by an axiom called sorryAx, so it shows up here. The Lean reference manual writes, as a checking procedure, "confirm that only the three standard axioms propext, Classical.choice and Quot.sound appear". The condition for the Lean label in this book has this form.

The meanings of the three are, in order, "equivalent propositions are equal", "an element can be extracted from a proof of existence (the axiom of choice)" and "equivalent elements are equal in the quotient". A quotient is the set obtained by lumping together the elements regarded as the same under an equivalence relation (the set of equivalence classes), for example the classes of remainders of integers divided by 7. The everyday reasoning of mathematics (including the law of excluded middle) needs nothing more than these three. For details, see 10-13 Lean statements and the limits of machine checking and "Axioms" in the guide.

On this machine we checked seven small files. Table 2 is the result.

Seconds are wall-clock time including loading import Mathlib (a 4-core machine, nice 19). Rows that load Mathlib take about 5 seconds for loading alone. The values are from one run in results.json and vary by about 10% from run to run (the exit codes, warnings and axiom rows are the same on re-running).

There are three things to read. First, a file containing sorry also passes with exit code 0. All that appears is a warning. If a checking record only says "no errors", the absence of sorry is not guaranteed. Second, native_decide creates one dedicated axiom just for that call. The Lean reference manual explains that this is so that what each axiom asserted can be audited individually. It differs by version: up to 4.28.0, every call appeared as depending on a common axiom Lean.ofReduceBool (with Lean.trustCompiler behind it). From 4.29.0, it changed to a dedicated axiom per call (of the form …ax_1_1 in Table 2). Axiom names change with the version, so this book judges by "is it a subset of the standard three?". Third, a false statement does not pass with decide.

Detour: using real numbers brings out the three axioms

Even with no holes and only the standard three axioms, something is still unchecked: whether the statement says what it means to say. At the start of its checking procedure, the Lean reference manual writes that it is important to distinguish the question "does the theorem have a correct proof?" from the question "what does the statement of the theorem mean?". The latter cannot be checked by machine.

This site's page 8 of the guide divides this gap into four types (Table 3).

② and ③ actually occur in the last two rows of Table 2. mass_gap_positive carries the name mass gap, but the statement is "a positive number is positive". To Lean a name is just a string and guarantees nothing about the content. This is why, when this book cites a theorem name, it writes the statement and the premises on the same line.

An example of ③ is the following statement.

The premises contradict each other, so the conclusion can be anything, and Lean passes it with a single linarith (an automatic step that combines linear inequalities). The more premises a theorem has, the harder this danger is to see. The way to check is to give one example that satisfies all the premises (a case where the answer is known, such as a free field). In Part 10 of this book, the role of an example satisfying all the premises is played by checking against the free field (10-16). Negative controls (10-13 Lean statements and the limits of machine checking) go the other way: they show that removing one assumption breaks the conclusion, confirming that the assumption is not decoration.

④ is the most important in this book. In a theorem that draws a conclusion from an unproved assumption such as Assumption H, the content is on the side of the assumption, and the theorem does not prove a single step of that assumption (10-13 Lean statements and the limits of machine checking).

A Lean theorem is a statement about typed objects. So looking at the types of a theorem's arguments tells you what the statement actually talks about. 10-13 Lean statements and the limits of machine checking divides the forty-six theorems that this book cites as conclusions into five layers by the types appearing in their statements. Exactly half, 23, are inequalities or identities of real numbers, and the theorems that have the lattice gauge field as a type are the 3 of 5-11.

Written as a formula, a sentence in this book with the Lean label consists of two parts.

Just as $C_P$ was a named real number in the example of §03, in many theorems of this book $C_P$, $\xi$ and $m$ are real variables. Reading them as physical quantities is done in the text, and whether that reading is right lies outside Lean. The conventions for the reading (the definition of $\beta$, the normalisation of tr, the metric of the lattice) are in 10-13 Lean statements and the limits of machine checking and A-01 Table of notation.

Why is there no theorem about the Wilson measure itself? One reason is stock. Counting words in the source of Mathlib, Lean's standard library of mathematics, in the version on this machine (the version is in Table 7 of §08) gave Table 4.

There are foundations for the uniform measure on a group (Haar measure), but the words of lattice gauge theory do not appear. The absence of a word is not a proof of the absence of a definition, but at least as named machinery, whoever uses it must build it from scratch. The guide's "Mathematics that mathlib has no stock of" divides the sources of such difficulty into three (quantity, way of stating, stock). The continuum limit and the construction of four-dimensional field theory lie beyond that (6-10).

Example. This site's paper (5-11) is one of the few examples that have the lattice gauge field as a type. Even there the Lean label is split by step: the chain from the action to a certain lower bound is Lean, and the step from that lower bound to the lattice mass gap is Paper (and only a sketch) (0-01).

Table 4b lists the bundles used in the assembly of the first step of Part 10, and Table 4c the bundles cited by Part 11. The rows are the same as Table 1 of 10-13; what a bundle guarantees is only the algebra, arithmetic and one-variable analysis from the list of assumptions to the conclusion. Every bundle follows the convention of writing the assumptions next to the theorem name (10-13 §04).

This book attaches labels sentence by sentence, not chapter by chapter or paper by paper, because even within one paper the label differs from step to step (the example in §06). Which label is attached is decided by the kind of guarantee the sentence has. Figure 2 puts that decision in the form of questions asked from the top down.

There is a reason for the order of the questions. The Lean label guarantees the arrow from premises to conclusion; the Known label refers to a proof in the literature, the Paper label to a proof on this book's side, the Computed label to a check over a finite range, and the Physics label to acceptance at the level of physics. The strong guarantees are asked first, and the first label that applies is attached. A sentence that matches none gets no label and is written as an "assumption" or a "question" (the questions of 10-17 carry no label).

When the sentences form a chain, read it as follows.

If just one step is Paper, then even if all the other steps are Lean, the conclusion is at the level of Paper. If the starting point $A_0$ is an assumption, the conclusion is also conditional on it. The premises $P_i$ of formula (1) correspond to this starting point.

This figure puts the conventions for labels in 0-01 in the form of questions. It contains no numbers.

How to read it. The Lean premise $C_P \le K\xi^2$ in the first row of the table is H↑, the upper half of the band statement $\text{H}_{\rm band}$ of the assumption in the last row (A-06 Index of assumptions). In the first row it is a premise; in the last row, the claim of an assumption. The labels differ because the roles in the sentence differ.

The Lean label presupposes that readers can check again on their own machines. The Lean reference manual describes checking as a staircase of four stages (Table 6). The lower stages are easier; the higher stages widen the range of doubt.

The manual itself positions stage 4 for high-risk settings, such as markets for proofs, competitions with large prizes, and AI whose intentions are not aligned. About stage 1, the manual warns that the check mark appears even if a dependency contains sorry. This is the same situation as gap_from_bound' in Table 2 having exit code 0, and it is why stage 2 is needed. The Lean labels in this book are attached to theorems that have been through at least stage 2.

The concrete procedure has the following form. How to install and match versions is in "Installing" in the guide and "Checking a distributed proof locally".

lake build                      # Stage 1: check the whole project
lake env lean File.lean         # check a single file only
#print axioms gap_from_bound    # Stage 2: write this inside the file

This site's Lean record (the list of theorems and the record of checking) is at the Lean record. Even the same proof may stop passing when the versions of Lean and Mathlib differ, because lemma names change. For this reason this book records the versions used for checking.

Finally, we gather into seven the things to ask when you receive a sentence with the Lean label. This is the checklist of "The procedure for reading a statement" in the guide, adapted to the way this book is read.

1. Is the theorem name given, so that you can check it again yourself (stage 1)?
2. Is there no sorry, and do the axioms fit within the three of formula (5) (stage 2)?
3. Have you followed every definition that appears in the statement (① of §05)?
4. Did you read the statement rather than the name (② of §05)?
5. Is one example satisfying all the premises given (③ of §05)?
6. Are the list of premises and the label of each premise written (④ of §05, formula (8))?
7. Where in the text is the reading of the real variables as physical quantities declared (§06, formula (7))?

The seventh is the question specific to this book. Many of the Lean theorems in this book connect to the mass gap problem only at this point, and that connection lies outside the Lean label.

What this chapter can say

Sources and reproduction

Next chapter to read: A-05 How this book was made — how sentences and numbers were checked before labels were attached.

← A-03 Guide to the literatureContentsA-05 How this book was made →