Lean in Practice: A Proof from the Inside

A Theorem You Already Know How to Prove

The preceding page treated formal methods from the outside — their history, their architecture, the structural reorganization of trust that proof assistants make possible. This page does the opposite. We pick a single theorem that every reader of the analysis section has already met, and we walk through its proof first in ordinary mathematical prose, then as a Lean script. The goal is to make the translation visible: not to teach Lean as a foreign language, but to show that the moves of tactic-mode proof are names for moves that any working mathematician already performs.

Surface syntax in this page reflects Lean 4 and mathlib as of May 2026. The translation between strategic moves and tactic invocations is structural; the specific keywords, tactic names, and mathlib lemma names that appear below may evolve while that structural correspondence remains.

The theorem is the triangle inequality for real numbers,

A reader who has worked through the real-analysis material has seen this several times. What matters here is not the result but the shape of the argument — the strategic decomposition a mathematician produces when asked to prove it. We will write that argument once, in full, with no reference to Lean. The same argument will reappear in the next section, annotated; and the section after that will exhibit it as Lean source.

The strategic decomposition

A useful characterization of the absolute value is the equivalence

valid for any real numbers \(a, b\) with \(b \geq 0\). Applied to the left-hand side of the triangle inequality with \(a = x + y\) and \(b = |x| + |y|\) — which is non-negative since absolute values are — the single inequality \(|x + y| \leq |x| + |y|\) becomes a pair of inequalities:

This is the first strategic move: use the characterization to split the goal into two parts. We now have two inequalities to prove, each simpler than the original because each is one-sided.

The two pieces

Consider the upper inequality \(x + y \leq |x| + |y|\). Two facts about the absolute value are immediate:

These hold for every real number — they are part of what absolute value means. Adding them gives \(x + y \leq |x| + |y|\), which is exactly the inequality we wanted. The argument for this piece is therefore: introduce two known facts, then perform a routine arithmetic step.

The lower inequality \(-(|x| + |y|) \leq x + y\) is symmetric. The corresponding facts are

which again hold for every real number. Adding them yields \(-(|x| + |y|) = -|x| + (-|y|) \leq x + y\), which is the inequality we wanted. Same shape of argument: introduce two known facts, perform a routine arithmetic step.

The complete argument, condensed

Reading back over what we just did, the proof has four strategic moves and nothing else:

1. Use the characterization \(|a| \leq b \iff -b \leq a \text{ and } a \leq b\) to replace the goal with a conjunction of two one-sided inequalities.
2. Decompose the conjunction into two independent goals — prove one, then prove the other.
3. For each goal, introduce the two relevant facts about absolute value (\(x \leq |x|\) and \(y \leq |y|\), or their negative analogues).
4. Close each goal with a routine arithmetic step combining the two facts.

Every step of this argument is a move that the reader has performed dozens of times in other proofs. None of the moves requires creative insight; the proof is, in the working mathematician's vocabulary, routine. That routineness is exactly what we will exploit. The moves listed above have names — names a proof assistant uses to mechanize them. The next section gives those names.

From Moves to Tactics

Each of the four moves identified at the end of the previous section has a name in Lean. Before we look at the Lean source as a whole, we walk down the list and pair each move with its name. The names will look unfamiliar on first encounter, but the substance behind each one is something the reader has already done in the proof above.

The four moves and their names

Move 1: Use a characterization to rewrite the goal. The mathematician's instinct, faced with \(|x + y| \leq |x| + |y|\), is to recall that \(|a| \leq b\) is equivalent to a conjunction of two simpler inequalities, and to apply that equivalence to transform the goal. The Lean tactic that performs this substitution along a known equivalence is rw (short for "rewrite"). Concretely, mathlib registers the equivalence \(|a| \leq b \iff -b \leq a \land a \leq b\) under the name abs_le, and the invocation rw [abs_le] replaces the goal \(|x + y| \leq |x| + |y|\) with the conjunction \(-(|x| + |y|) \leq x + y \land x + y \leq |x| + |y|\).

Move 2: Decompose a conjunction into its two parts. Having a single goal of the form \(P \land Q\), the mathematician separates the two pieces and addresses them independently. The Lean tactic for this is constructor. After constructor, what was a single goal \(P \land Q\) becomes two subgoals — \(P\) and \(Q\) — each addressed on its own.

The connection back to formal methods is direct. A proof of \(P \land Q\) is, under the correspondence between propositions and types, a pair whose components are proofs of \(P\) and \(Q\). The constructor tactic is the instruction to build that pair by constructing each component separately.

Move 3: Introduce a known fact as a named premise. When the mathematician writes "we know that \(x \leq |x|\)" and proceeds to use this fact, the act is one of bringing an external lemma into the local context and giving it a name. The Lean tactic for this is have. The syntax have h : x ≤ |x| := le_abs_self x reads almost as English: "let \(h\) be the fact that \(x \leq |x|\), which holds by the mathlib lemma le_abs_self applied to \(x\)." After this line, \(h\) is available as a hypothesis for the rest of the current goal.

The mathlib name le_abs_self is not a code one needs to memorize. It is built from English fragments according to a regular convention: a statement of the form \(a \leq \text{something}(a)\) reads as a is less-than-or-equal to something of a, and mathlib's lemma names are written in that order. Most lemmas one wants to use in a Lean proof can be guessed or discovered interactively, a point we return to in the final section.

Move 4: Close the goal by routine arithmetic. The final step in each branch of the proof is to combine two facts of the form \(a \leq b\) by addition. This is the kind of arithmetic that a mathematician performs without comment, and it is also the kind of step that Lean is willing to perform without comment. The tactic linarith (short for "linear arithmetic") closes any goal that follows from the linear-arithmetic combination of available hypotheses. Given the hypotheses \(-|x| \leq x\) and \(-|y| \leq y\), the goal \(-(|x| + |y|) \leq x + y\) follows linearly, and linarith dispatches it.

Tactics as named moves, not foreign vocabulary

The four tactics just introduced — rw, constructor, have, linarith — are not language features that one learns the way one learns the syntax of a new programming language. Each is the name of a move that already has an intuitive content for the reader:

• rw [name] — rewrite the goal using the named equivalence or equality
• constructor — split a structured goal into its constituent subgoals
• have h : P := proof — introduce a named fact into the local context
• linarith — close the goal by linear arithmetic over the current hypotheses

Each entry of this list paraphrases the corresponding move from the strategic decomposition. The Lean tactic does mechanically what the mathematician's prose does in words. Tactic mode, in this sense, is not a separate skill from proof construction; it is a notation for proof construction at the strategic level, with the bookkeeping handled by the system.

The shape of a Lean theorem

Before we write the full Lean proof, three pieces of syntax need to be visible. A theorem in Lean has the form

theorem name (arg₁ : T₁) (arg₂ : T₂) : statement := proof

The pieces are: the keyword theorem, a name chosen by the author, parenthesized arguments with their types, a colon separating the arguments from the statement being proved, and the symbol := separating the statement from its proof. The proof itself can be a single term written directly (as we saw on the preceding page) or — when the proof is constructed by tactics — the keyword by followed by an indented sequence of tactic invocations.

When a tactic-mode proof has multiple subgoals open (as it will after constructor), the convention is to focus on each subgoal in turn using the bullet symbol ·. Each bulleted block addresses one subgoal; once that subgoal is closed, the next bullet picks up the next subgoal. This is the only syntactic detail of tactic-mode proofs that the next section will require.

With these pieces in place, the four moves translate directly into a Lean script. The next section exhibits the script and walks through what happens at each step.

The Translation in Full

Here is the complete Lean proof. After the script, we walk through it line by line, showing the proof state at the points where the state changes shape.

                    theorem triangle_inequality (x y : ℝ) : |x + y| ≤ |x| + |y| := by
                    rw [abs_le]
                    constructor
                    · have h1 : -|x| ≤ x := neg_abs_le x
                        have h2 : -|y| ≤ y := neg_abs_le y
                        linarith
                    · have h1 : x ≤ |x| := le_abs_self x
                        have h2 : y ≤ |y| := le_abs_self y
                        linarith
                

Each tactic invocation in this script corresponds to one move in the strategic decomposition of the previous section. The rewriting along the characterization, the splitting of the conjunction, the introduction of named facts, the closing arithmetic — each appears once per branch, in the order the mathematician would perform it. The correspondence between strategic moves and tactic invocations is one-to-one. That correspondence is not an accidental feature of this particular proof; it is the design intent of tactic mode itself.

The state at the start

Before any tactic has been applied, Lean shows the proof state as

x y : ℝ
⊢ |x + y| ≤ |x| + |y|

The hypotheses appear above the horizontal turnstile ⊢, the goal below. At this moment the local context contains the two real variables x and y, and the goal is the inequality we set out to prove.

After rw [abs_le]

The tactic rw [abs_le] rewrites the goal along the equivalence \(|a| \leq b \iff -b \leq a \land a \leq b\). After this tactic, the proof state becomes

x y : ℝ
⊢ -(|x| + |y|) ≤ x + y ∧ x + y ≤ |x| + |y|

The goal is now a conjunction. Both sides remain to be proved, and we have committed to no particular strategy beyond the application of the characterization. The substantive content of this step is the move from "prove an absolute-value inequality" to "prove two simpler one-sided inequalities."

A small notational remark is worth making here. The mathematician's prose in the opening section stated the characterization \(|a| \leq b \iff -b \leq a \land a \leq b\) under the hypothesis \(b \geq 0\), as is customary in analysis textbooks. The mathlib lemma abs_le drops this hypothesis: it asserts the iff for all \(a, b\) without qualification. The two statements are mathematically compatible — when \(b < 0\), the left-hand side \(|a| \leq b\) is false (because absolute values are non-negative) and the right-hand side \(-b \leq a \land a \leq b\) is also false (because it would require \(-b \leq a \leq b\) with \(-b > 0 > b\)), so the iff holds vacuously. Library design in mathlib favors the unconditional form because it requires no hypothesis to invoke. The mathematician's prose and the library's formulation describe the same fact, registered for different purposes.

After constructor

The tactic constructor takes the conjunction goal and produces two subgoals, one for each conjunct. The first subgoal — labelled case left — becomes the active proof state:

case left
x y : ℝ
⊢ -(|x| + |y|) ≤ x + y

A second subgoal labelled case right remains pending behind it; once the left subgoal is closed, that second subgoal will become active in turn. The bullet · on the next line of the script focuses on the first subgoal. Once that subgoal is closed, the bullet on a later line picks up the second subgoal. This is the structural counterpart of the mathematician's "first we prove this, then we prove that" — Lean asks the author to handle the two parts in visibly separate blocks.

After the two have lines in the first branch

Inside the first bullet, the lines

  have h1 : -|x| ≤ x := neg_abs_le x
  have h2 : -|y| ≤ y := neg_abs_le y

introduce the two facts about the absolute value that the first branch requires. The mathlib lemma neg_abs_le applied to x produces a proof of \(-|x| \leq x\), which is bound to the name h1; similarly for h2. After these two lines the proof state is

                    case left
                    x y : ℝ
                    h1 : -|x| ≤ x
                    h2 : -|y| ≤ y
                    ⊢ -(|x| + |y|) ≤ x + y
                

The local context has gained two named hypotheses. The goal is unchanged. We are now in the position the mathematician was in halfway through the first branch of the prose argument: two known facts at hand, one combination away from the conclusion.

The closing linarith

The tactic linarith searches for a proof of the current goal by linear arithmetic over the hypotheses available in the local context. Given h1 and h2 as above, the inequality \(-(|x| + |y|) \leq x + y\) follows by adding h1 and h2 and rearranging — a manipulation entirely within the scope of linear arithmetic. The tactic finds the proof and closes the goal.

The second branch (handling the case \(x + y \leq |x| + |y|\)) proceeds identically with the symmetric lemmas. After the closing linarith of that branch, no goals remain and the proof is complete.

Partial proofs and the role of sorry

One feature of Lean that is worth seeing even in a first encounter is the keyword sorry. A reader constructing the proof above for the first time might want to establish the overall structure before filling in the details — to see whether the rewriting, the case split, and the introduction of named hypotheses are correctly arranged, and only afterward worry about whether linarith actually closes each goal. Replacing the final tactic in each branch with sorry produces a script that Lean accepts as a proof outline:

                    theorem triangle_inequality (x y : ℝ) : |x + y| ≤ |x| + |y| := by
                    rw [abs_le]
                    constructor
                    · have h1 : -|x| ≤ x := neg_abs_le x
                        have h2 : -|y| ≤ y := neg_abs_le y
                        sorry
                    · have h1 : x ≤ |x| := le_abs_self x
                        have h2 : y ≤ |y| := le_abs_self y
                        sorry
                

Lean reports two warnings — one for each sorry — but otherwise accepts the script. The author has demonstrated, to the system and to themself, that the strategic skeleton is sound. The arithmetic steps remain to be filled in, but their place in the proof is fixed. This top-down style of proof construction, with sorry as a placeholder for "the rest will follow," is one of the principal ways that Lean proofs are written in practice.

What happens when something goes wrong

Suppose the author types le_abs_self where neg_abs_le was meant. The line

  have h1 : -|x| ≤ x := le_abs_self x

asks Lean to bind h1 to a proof of \(-|x| \leq x\), but offers a term whose type is \(x \leq |x|\). The types do not match, and Lean reports the mismatch. The error is not a punishment for making a mistake; it is information about where the script's stated intent and its actual content have come apart. The author either repairs the lemma name or repairs the stated type — whichever was wrong — and the script proceeds.

This back-and-forth is the working rhythm of tactic-mode proof construction. The proof is rarely written from top to bottom in a single pass. The author writes, the system reports states and errors, the author adjusts. What looks on the page like a static sequence of tactics is the residue of a dialogue.

The Verification Loop

The proof on the page exists inside an ecosystem. Every named lemma that appeared in the previous section — abs_le, le_abs_self, neg_abs_le — was an entry in mathlib, the community-maintained library of theorems formalized in Lean. This final section describes the role of that library and the working practices that surround it, and then returns to the question of what we have and have not done by writing the proof.

mathlib as ambient context

A Lean file written in isolation has no theorems available to it. A file that begins with import Mathlib inherits the entire library — every theorem of undergraduate real analysis, linear algebra, group theory, point-set topology, and a substantial portion of graduate-level material besides. The triangle-inequality proof in the previous section rested on mathlib at every step: the equivalence abs_le, the lemmas le_abs_self and neg_abs_le, the decision procedure inside linarith, and the definition of the absolute value itself.

The practical consequence is that authoring a proof in Lean is, much of the time, an exercise in finding the right name. A mathematician proving the triangle inequality with pen and paper does not need to know that le_abs_self is the name of the fact \(x \leq |x|\); they need only to know the fact itself. A mathematician proving the same theorem in Lean needs to know — or to find — the name under which the fact is registered.

Searching the library

Lean provides tactics for searching mathlib from inside a proof in progress. The tactic exact?, placed where a closing term would go, asks Lean to search for a library lemma that closes the current goal directly. The tactic apply? searches for a lemma whose conclusion matches the goal up to the introduction of new subgoals. External tools such as Loogle accept a description of a lemma's shape — its pattern of quantifiers, hypotheses, and conclusion — and return matching candidates from mathlib's index.

A working session in Lean therefore alternates between two activities: writing tactics that encode strategic moves, and querying the library for the specific lemmas those moves require. The author moves between a local view of the proof under construction and a global view of what facts mathlib has already established. The library is large enough that most of the lemmas an undergraduate analysis course will use are already present; it is also large enough that knowing how to search it is itself a substantial skill, of a piece with the skill of constructing the proof.

The same theorem, in one line

A search of mathlib for the triangle inequality returns it as the lemma abs_add_le, whose statement is exactly \(\forall a\, b : \mathbb{R},\ |a + b| \leq |a| + |b|\). With this lemma in hand, the entire proof reduces to one line:

theorem triangle_inequality (x y : ℝ) : |x + y| ≤ |x| + |y| := abs_add_le x y

The proof term is abs_add_le x y — the library lemma applied to the two specific real numbers. No tactic mode, no have, no linarith. A mathlib library of over two hundred thousand theorems would not omit a result this basic; the one-line proof is the realistic Lean style for any theorem already in the library.

The reconstruction in the previous section was therefore not the proof that a working Lean user would write in practice. It was a reconstruction as if the relevant lemmas — but not the theorem itself — were available. That reconstruction had a pedagogical purpose: to exhibit the translation between strategic moves and tactic invocations on a theorem familiar enough that the strategic moves themselves required no explanation. A practitioner who encounters the same theorem in their own work looks first to mathlib; only when the relevant result is absent does the longer reconstruction become the actual workflow. Most of working with Lean is the alternation between these two regimes — finding what is already there, and proving what is not.

What the kernel verified

Once the proof was written and accepted, the verifying agent was not the tactic framework, not the linarith decision procedure, not mathlib. Tactics build candidate proof terms; the kernel inspects those terms. A buggy tactic that produces an ill-typed term, or a tactic that gestures at a proof without actually constructing the required term, cannot bypass the kernel — the kernel re-checks each term against the proposition with no reference to how the term was produced. This is the structure that the preceding page laid out under the name of the de Bruijn criterion. The triangle-inequality proof is an instance of it.

The instance is worth pausing over. The script in the previous section was authored by a person working out a strategy in informal mathematical prose, then translating that strategy into named tactic invocations. Nothing in that authoring process was verified by Lean. The verification began only at the moment the script was submitted to the kernel. The same script, had it been authored by some other agent — by a different mathematician, by a machine, by an automated proof-search routine — would have been verified by exactly the same procedure to exactly the same standard. The kernel reads the term; the kernel accepts or rejects.

This is the operative content of the distinction, drawn on the preceding page, between proof verification and proof discovery. Discovery is what the human did in the opening section, in informal prose, before any Lean tactic was invoked. Verification is what the kernel did, after the script was complete, by inspecting the proof term that the tactics produced. The two activities are separable, and Lean's architecture insists on the separation. A formal proof, in the modern sense, is not a proof that a human has been relieved of constructing; it is a proof whose construction is open to any agent capable of producing a verifiable term, while the standard of correctness remains fixed at the kernel.

What remains, and what does not

What the kernel verified was the implication: given the propositions registered in mathlib as abs_le, le_abs_self, and neg_abs_le, and given the soundness of linarith's linear-arithmetic procedure, the assertion \(|x + y| \leq |x| + |y|\) holds for all real \(x, y\). The kernel did not verify that the mathlib lemmas are themselves correctly stated, nor that they capture what the author of those lemmas intended. Those verifications happened earlier — when each lemma was added to mathlib and reviewed by the library's contributors — and they too rest, at bottom, on the same kernel. The trust chain bottoms out where the preceding page said it bottoms out: in the kernel implementation, and in the human review of specifications.

A reader who has followed the construction from the strategic decomposition through the tactic translation to the kernel-verified term has now seen, in one example, what a proof-assistant proof actually is. It is not a proof that the system found; it is a proof that the system checked. The thinking is human; the bookkeeping is mechanical; the verification is structural. Subsequent encounters with Lean in the curriculum — and there will be encounters, as the mathematical and computer-science material in later sections grows in technical weight — will take this shape as given. The triangle inequality is the smallest example that exhibits all the moving parts.