Lean in Practice: Proof from the Inside

A Theorem We Already Know How to Prove

The preceding page treated formal methods from the outside, through their history, their architecture, and 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.

What matters here is not the result but the shape of the argument. By this we mean the strategic decomposition a mathematician produces when asked to prove it.

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. In the working mathematician's vocabulary, the proof is routine. That routineness is exactly what we will exploit. The moves listed above have names, which 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 the English sentence "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.

The four tactics just introduced, namely rw, constructor, have, and 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 the mathematician's prose has already named in words. The Lean tactic does mechanically what the 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, and the tactics inside it are aligned with the first tactic after the bullet symbol, which is how Lean tells where the block ends. Once that subgoal is closed, the next bullet picks up the next subgoal. Bullets are the only syntactic detail of tactic-mode proofs that the next section will require.

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
                    

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 line marked by the turnstile ⊢, and the goal follows the turnstile. 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."

One small notational remark is in order. The mathematician's prose in the opening section stated the characterization under the hypothesis \(b \geq 0\), as is customary in analysis textbooks. The mathlib lemma abs_le drops this hypothesis. The unconditional form is equivalent and requires no precondition to invoke.

After constructor

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

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

A second subgoal labeled 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, and the bullet on a later line picks up the second one after the first is closed. 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, and 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.

                        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
                    

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

The Verification Loop

The proof on the page exists inside an ecosystem. Every named lemma that appeared in the previous section, namely abs_le, le_abs_self, and 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 that imports nothing has only the basic facts of Lean's core library, about natural numbers, lists, and logic. A file that begins with import Mathlib inherits the entire library, which covers most of the standard results of undergraduate real analysis, linear algebra, group theory, and 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.

Authoring a proof in Lean is, much of the time, an exercise in finding the right name. Knowing the fact is not enough, since one needs the label under which mathlib has registered it.

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 and return matching candidates from mathlib's index. The shape is the lemma's pattern of quantifiers, hypotheses, and conclusion.

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.

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

What remains, and what does not

What the kernel verified was a proof term deriving \(|x + y| \leq |x| + |y|\) for all real \(x, y\) from the mathlib lemmas abs_le, le_abs_self, and neg_abs_le, together with the term that linarith constructed. No trust in linarith is needed, since its output was checked like every other term. The proofs of the mathlib lemmas were checked by the same kernel when the library was built. What the kernel did not verify is that these lemmas, and the theorem statement itself, say what their authors intended. That question is settled by the library's contributors, who reviewed each lemma when it was added to mathlib. 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 but a proof that the system checked. The thinking is human, the bookkeeping is mechanical, and the verification is structural. The triangle inequality is the smallest example that exhibits all the moving parts.