The whole guide

Glossary

43 terms that appear in this guide. General terms come first, then symbols and identifiers, each group in alphabetical order (the Japanese original sorts its general terms in the 50-sound syllabary order). The right-hand column points to the page that treats the term in detail.

General terms

Term	Meaning	Detail
axiom	A proposition accepted without proof. The ones that ordinarily appear with Lean and mathlib are three: `propext`, `Classical.choice`, `Quot.sound`. Which ones a theorem relies on, the machine answers theorem by theorem.	01
certificate	The answer found by a search, written out in a form that is easy to check: the shape of a tree, integer upper and lower bounds, a table of a map, and so on. The search itself is done outside Lean; only the certificate is handed to Lean to confirm.	07
concatenated version	A proof spread over several files, joined into a single file in dependency order. Used when the recipient wants to re-check the whole thing in one pass in their own environment.	09
exhaustive enumeration	Listing every candidate without exception. Lean can say that the candidates listed fail the condition; that the candidates are exhausted by the list is, in most cases, outside the Lean theorem.	09 · 10
hole	An unfinished spot in a proof. In Lean you leave it by putting `sorry`. A theorem with one shows `sorryAx` under `#print axioms` and is in a state of claiming nothing.	01
hypothesis	A condition a theorem takes as a premise. In Lean it is written as an argument, so printing the statement with `#check` shows all of them. Every hypothesis added makes the theorem weaker, which is why you count them when reading.	08 · 09
machine check	The kernel confirming that a proof term really has the type it claims. What is guaranteed is only that "the statement as written follows from the definitions as written and the axioms listed".	01
negative control	Deliberately writing in Lean that the statement becomes false when a hypothesis is removed, to confirm it. Placed to catch a definition so strong that anything goes through, or an unnecessary hypothesis that has crept in.	09
proposition	A statement whose truth can be asked. In Lean it is written as a type, and that type belongs to `Prop`.	01
term	An expression that has a type. A proof is a term. Using a lemma is written in the same form as passing arguments to that lemma's term.	01
theorem	A named proposition together with its proof, declared with `theorem`. The theorem name is attached to the Lean label so that following the name lets you read the statement.	09
three standard axioms	`propext`, `Classical.choice`, `Quot.sound`. That the axioms relied on stay within these three is one of the conditions for the Lean label.	01
type	What expresses the kind of an object or a proposition. In Lean a proposition is itself a type, and a term of that type is a proof. `ℕ` (natural numbers), `ℚ` (rationals), and `ℝ` (reals) are types too.	01

Symbols and identifiers

Term	Meaning	Detail
`Classical.choice`	The axiom of choice. From a nonempty type you can pick out an element. It is where the law of excluded middle comes from, so it enters whenever you argue by contradiction.	01
`decide`	A tactic that runs a decision procedure in the kernel to close a proposition. Usable only on propositions that carry a `Decidable` instance. On a large object it stops on unfolding depth or memory.	03
`Decidable`	The type class saying that the truth of the proposition can be settled by a finite procedure. Whether `decide` can be used is determined by whether this is attached. If it is not, you write it yourself.	03 · 11
`elan`	The tool that manages Lean versions. It reads the single line in the project's `lean-toolchain` and fetches that version automatically if needed.	02
`exact?` `apply?`	Tactics that search mathlib for a lemma that closes the goal outright, or one that can be applied in combination with the hypotheses. Copy the term they find into place and do not leave the call in the proof.	02
`Finset`	The type of finite sets. You get the cardinality `#s`, the sum `∑ x ∈ s, f x`, and the filter `s.filter p`. A count can be made the object of a proof as it stands.	04
`Fintype`	The type class saying that the type has finitely many elements and all of them can be listed. `Fintype.card` gives the number of elements, and `∀` and `∃` become decidable.	04
kernel	The small core that does nothing but type checking. Every term a tactic assembles must pass through here at the end. What you have to trust is only the kernel's implementation, the axioms, and how the proposition is written.	01
`lake`	The tool that fetches dependencies and builds. `lake exe cache get` fetches prebuilt oleans for mathlib, and `lake build` builds in order.	02
`lake env lean`	How to check a single file. `lake env` sets the locations of the dependencies in environment variables, then runs `lean` on top of that. Empty output means it passed.	02
`lakefile.toml` `lake-manifest.json` `lean-toolchain`	The three project files. In order: the name and the declared dependencies; the pinned revisions of the dependencies; the Lean version. Reproducing a result needs all three; "checked with Lean 4" is not enough.	02
`LEAN_NUM_THREADS`	The environment variable that sets how many files are built at once. In a project where a single proof uses several GB, you have to throttle it or memory runs out and nothing moves.	02 · 11
`linarith`	A tactic that closes a linear inequality as a linear combination of the given hypotheses. Nonlinear terms have to be replaced beforehand.	06
Mathlib	The mathematics library for Lean 4, made up of more than 8,000 files. Lemma names and definitions both move between revisions, so pin the revision when you distribute.	02
`maxRecDepth`	The cap on the depth of term unfolding. Applying `decide` to a large object stops with `maximum recursion depth has been reached`. Raising it sometimes gets you further, but changing how you write it is usually faster.	01 · 11
`native_decide`	A tactic that compiles the decision procedure to machine code, runs it, and accepts the result as an axiom. Fast, but the range of trust widens to the compiler and the execution environment. Not used on this site.	01
`norm_num`	A tactic that brings an expression containing numerals into normal form and closes it. Strong on concrete numerical equalities and inequalities.	01
olean	An intermediate file holding checked declarations. Read at `import` time. Fetching mathlib's saves rebuilding from source.	02
`omega`	A tactic that closes linear arithmetic over the integers and natural numbers by a decision procedure. Addition, subtraction, multiplication by constants, `≤`, and some remainders. It handles the truncation of natural-number subtraction correctly.	11
`Prop`	The universe that the types of propositions belong to. The elements of `Prop` are propositions, and the elements of a proposition are its proofs.	01
`propext`	The axiom of propositional extensionality. Two propositions that are equivalent are equal. Rewriting a proposition as an equation relies on it, so it enters almost whenever you use `simp`.	01
`Quot.sound`	The axiom of quotient soundness. When you take a quotient, equivalent representatives are equal. It enters when you touch a type built as a quotient, such as the rationals or finite multisets.	01
`rfl`	The term asserting that both sides come to the same form when definitions are unfolded. Uses no axioms at all. It stops working when the symmetry of a definition breaks (`n + 0` closes, `0 + n` does not).	02
`ring`	A tactic that closes an equation in a commutative ring by expanding and collecting. When fractions are involved, clear the denominators with `field_simp` before applying it.	11
`simp`	A tactic that simplifies an expression by applying rewrite rules repeatedly. It uses the rule set mathlib carries. `simp?` prints which rules it used.	11
`sorry`	A hole in a proof. Putting one in produces the warning declaration uses `sorry`, and the check itself carries on. You miss it if you look only at errors.	01
`sorryAx`	The axiom that `sorry` introduces. It proves every proposition, so a theorem in which it appears says nothing.	01
tactic	A program that assembles a proof term. Written after `by`. The kernel checks the term it built, so a mistake in a tactic does not necessarily become a mistake in the theorem. Conversely, a tactic failing does not make the proposition false.	01
`#check` `#eval`	Print the type of a term; compute and print its value. Passing a theorem name to `#check` prints the statement as is. The result of `#eval` is not a proof: it does not go through the kernel, so it carries the same weight as computation.	02
`#print axioms`	Lists the axioms the theorem relies on. The surest way to find holes (`sorryAx`) and `native_decide`. For a theorem that uses no axioms, the wording changes to `does not depend on any axioms`.	01

The common tactics on one sheet

The tactics from the table above, each next to the kind of goal it is good at.

import Mathlib

-- Confirm a Decidable instance is present, then apply decide
example : Decidable (3 ∣ 12) := by infer_instance
theorem three_dvd_twelve : 3 ∣ 12 := by decide

-- Finset and Fintype
#eval (Finset.range 10).filter (fun n => n % 3 = 0)
#eval (Finset.range 10).sum id
#eval Fintype.card (Fin 5 × Fin 3)

-- simp (rewriting by rules)
example (x : ℕ) : x + 0 = x := by simp

-- ring (equations in a commutative ring)
example (x y : ℤ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by ring

-- omega (linear arithmetic over integers and naturals)
example (a b : ℕ) (h : a + 3 ≤ b) : a < b := by omega

-- linarith (closing an inequality by a linear combination of hypotheses)
example (x y : ℝ) (h1 : x ≤ y) (h2 : 0 ≤ x) : 0 ≤ 2 * y := by linarith

-- norm_num (concrete numerical expressions)
example : (7 : ℝ) / 2 < 4 := by norm_num

The output of the three #eval lines:

{0, 3, 6, 9}
45
15

The remaining declarations produce no output. As in 02, empty output is what "it passed" means.

Sources and reproduction

Item	Kind	Source or tool
The code snippet and output in §03	machine check	Checked with Lean 4.33.1 and mathlib (revision `0df444a3…`); output copied verbatim
Names and roles of the axioms and tactics	known	The Lean 4 core and mathlib
The axioms the theorems on this site rely on	machine check	The ledger in the Lean verification bundle

Revised 2026-09-20: first version. 43 terms.