← Lean

Chapter 6, line by line

Induction. The theorem is Example 6.1.2 in How To Prove It: 3 divides n3 + 2n for every natural number n. In the package it is Like_Example_6_1_2, in HTPILib/Chap6.lean, and the proof below is Velleman's, copied without changes.

Two things make this the right example. First, the induction step needs a genuine algebraic identity, so you get to see how Lean handles routine algebra (it does it for you, with ring). Second, the divisibility is a hidden existential, so Chapter 3 shows up again inside Chapter 6, which is the honest structure of the subject.

What by_induc does

A goal of the form ∀ (n : Nat), P n is a universally quantified statement, so you could try fix n : Nat and prove P n directly. Usually you cannot. by_induc is the alternative: it replaces the single goal with two goals.

Before 
⊢ ∀ (n : Nat), 3 ∣ n ^ 3 + 2 * n
After by_induc: goal 1, the base case 
⊢ 3 ∣ 0 ^ 3 + 2 * 0
After by_induc: goal 2, the induction step 
⊢ ∀ (n : Nat), 3 ∣ n ^ 3 + 2 * n → 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)

These two states are reconstructed from the tactics that follow in Velleman's proof (they are forced by it), not quoted from his file.

That is the entire principle of mathematical induction, expressed as a single legal move. And look carefully at goal 2, because it answers the question every student asks in week eleven:

"Isn't assuming P(n) assuming what we're trying to prove?" No, and here is the proof that it is not. The thing being proved is ∀ n, P n → P (n + 1). That is a statement about a conditional. Assuming P n in order to derive P (n + 1) is just the ordinary Chapter 3 move for a conditional goal — the same assume you have been using since September. The induction hypothesis is not an assumption of the theorem; it is the antecedent of the implication you are currently proving. Lean's display makes this impossible to misread, which is why doing one of these in Lean tends to settle the question permanently.

The two goals are handled by the two · bullets in the proof below. Everything indented under the first bullet is the base case; everything under the second is the induction step. Nothing but indentation keeps them apart, so mind the whitespace.

Example 6.1.2

On paper

Base case. 03 + 2·0 = 0 = 3·0, so 3 ∣ 0.

Induction step. Let n be arbitrary and suppose 3 ∣ n3 + 2n.

Then n3 + 2n = 3k for some k.

Now (n+1)3 + 2(n+1) = n3 + 2n + 3n2 + 3n + 3 = 3k + 3n2 + 3n + 3 = 3(k + n2 + n + 1),

so 3 ∣ (n+1)3 + 2(n+1).

By induction, the result holds for all n. □

In Lean

theorem Like_Example_6_1_2 :
    ∀ (n : Nat), 3 ∣ n ^ 3 + 2 * n := by
  by_induc
  · -- Base Case
    define         --Goal : ∃ (c : Nat), 0 ^ 3 + 2 * 0 = 3 * c
    apply Exists.intro 0
    rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : 3 ∣ n ^ 3 + 2 * n
    define at ih   --ih : ∃ (c : Nat), n ^ 3 + 2 * n = 3 * c
    obtain (k : Nat) (h1 : n ^ 3 + 2 * n = 3 * k) from ih
    define         --Goal : ∃ (c : Nat), (n + 1) ^ 3 + 2 * (n + 1) = 3 * c
    apply Exists.intro (k + n ^ 2 + n + 1)
    show (n + 1) ^ 3 + 2 * (n + 1) = 3 * (k + n ^ 2 + n + 1) from
      calc (n + 1) ^ 3 + 2 * (n + 1)
        _ = n ^ 3 + 2 * n + 3 * n ^ 2 + 3 * n + 3 := by ring
        _ = 3 * k + 3 * n ^ 2 + 3 * n + 3 := by rw [h1]
        _ = 3 * (k + n ^ 2 + n + 1) := by ring
    done
  done

Verbatim from HTPILib/Chap6.lean (Velleman), his comments included.

The base case, step by step

define

English: "3 divides 0 means: there is a c with 0 = 3c."
What it does: unfolds ∣. Divisibility is a definition, and the definition is existential. This is the moment Chapter 3 walks back into the room.

Velleman's own comment 
Goal : ∃ (c : Nat), 0 ^ 3 + 2 * 0 = 3 * c

apply Exists.intro 0 then rfl

Supply the witness — c = 0 — and then the remaining goal is 0 ^ 3 + 2 * 0 = 3 * 0, which both sides compute to 0. rfl ("reflexivity") closes any goal whose two sides are literally the same after computation. For concrete numbers, Lean just does the arithmetic.

The induction step, step by step

fix n : Nat and assume ih : 3 ∣ n ^ 3 + 2 * n

The goal was ∀ n, P n → P (n + 1). Universal goal, so fix; conditional goal, so assume. There is nothing induction-specific happening here at all, which is the point made in the box above. The name ih is a convention, not a keyword — you could call it h7.

Tactic state after 
n : Nat
ih : 3 ∣ n ^ 3 + 2 * n
⊢ 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)

Reconstructed from the surrounding tactics, not quoted from Velleman's file.

define at ih and obtain (k : Nat) (h1 : ...) from ih

English: "So n3 + 2n = 3k for some k."
What it does: unfold the divisibility in the hypothesis, exposing an existential; then obtain strips the existential and hands you a name for the witness plus the fact about it. This is the Chapter 3 move for an existential given, and it is the reason the divisibility exercises are a good first induction: you get to use both halves of Chapter 3's existential machinery in a single proof.

Velleman's comment, then the effect of obtain 
ih : ∃ (c : Nat), n ^ 3 + 2 * n = 3 * c
k : Nat
h1 : n ^ 3 + 2 * n = 3 * k

define and apply Exists.intro (k + n ^ 2 + n + 1)

Unfold the divisibility in the goal, then supply the witness. And here is the actual mathematical content of the whole proof: you have to know what c is before you can start computing.

Velleman's own comment 
Goal : ∃ (c : Nat), (n + 1) ^ 3 + 2 * (n + 1) = 3 * c

On paper you discover c = k + n2 + n + 1 by doing the algebra and reading off the answer at the end. Lean makes you commit to it first, then verify. That is a real difference in workflow and it is worth naming: do the scratch algebra on paper, then write the Lean proof knowing the answer. Trying to discover the witness while inside Lean is miserable and is not what the tool is for.

The calc block

The chain of equalities, one line per equals sign, with a justification after each :=. The underscore means "the right-hand side of the line above." 

      calc (n + 1) ^ 3 + 2 * (n + 1)
        _ = n ^ 3 + 2 * n + 3 * n ^ 2 + 3 * n + 3 := by ring
        _ = 3 * k + 3 * n ^ 2 + 3 * n + 3 := by rw [h1]
        _ = 3 * (k + n ^ 2 + n + 1) := by ring

Verbatim excerpt from HTPILib/Chap6.lean (Velleman).

Two justifications appear. ring proves any identity that holds in every commutative ring by normalizing both sides — expanding (n + 1) ^ 3, collecting terms, all of it. You do not check that step and you do not have to. rw [h1] substitutes using the induction hypothesis, replacing n ^ 3 + 2 * n by 3 * k.

Notice the shape: algebra, then the induction hypothesis, then algebra. The middle line is the only one that uses induction at all, and the outer two are bookkeeping that the machine does. That decomposition is invisible in the paper proof, where the whole computation is one displayed chain, and seeing it separated is genuinely clarifying about what induction contributes.

A summation, and an inequality

Two more of Velleman's, verbatim, because the other two things Chapter 6 asks you to do by induction are sums and inequalities, and each has one wrinkle.

A sum

theorem Like_Example_6_1_1 :
    ∀ (n : Nat), (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1) := by
  by_induc
  · -- Base Case
    rewrite [sum_base]
    rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1)
    show (Sum i from 0 to n + 1, 2 ^ i) + 1 = 2 ^ (n + 1 + 1) from
      calc (Sum i from 0 to n + 1, 2 ^ i) + 1
        _ = (Sum i from 0 to n, 2 ^ i) + 2 ^ (n + 1) + 1 := by
              rw [sum_from_zero_step]
        _ = (Sum i from 0 to n, 2 ^ i) + 1 + 2 ^ (n + 1) := by ring
        _ = 2 ^ (n + 1) + 2 ^ (n + 1) := by rw [ih]
        _ = 2 ^ (n + 1 + 1) := by ring
    done
  done

Verbatim from HTPILib/Chap6.lean (Velleman).

The wrinkle is that Sum i from 0 to n, f i is a defined notation, and peeling one term off the end is a theorem, not a manipulation. That theorem is sum_from_zero_step, and it says exactly what you would want: 

theorem sum_from_zero_step {A : Type} [AddZeroClass A] {n : Nat} {f : Nat → A} :
    Sum i from 0 to (n + 1), f i = (Sum i from 0 to n, f i) + f (n + 1)

Verbatim from the header comment of HTPILib/Chap6.lean (Velleman); the theorem itself lives in Chap8Part1.

sum_base is its companion for the one-term sum. On paper, "… the sum up to n+1 is the sum up to n plus the last term" is a sentence you write without thinking. In Lean it is a named lemma you rewrite with. This is a fair summary of the whole experience of formalizing: the steps are the same steps, and the ones you never noticed turn out to have names.

An inequality, and a base case that is not zero

theorem Example_6_1_3 : ∀ n ≥ 5, 2 ^ n > n ^ 2 := by
  by_induc
  · -- Base Case
    decide
    done
  · -- Induction Step
    fix n : Nat
    assume h1 : n ≥ 5
    assume ih : 2 ^ n > n ^ 2
    have h2 : n * n ≥ 5 * n := Nat.mul_le_mul_right n h1
    show 2 ^ (n + 1) > (n + 1) ^ 2 from
      calc 2 ^ (n + 1)
        _ = 2 * 2 ^ n := by ring
        _ > 2 * n ^ 2 := by linarith
        _ ≥ n ^ 2 + 5 * n := by linarith
        _ > n ^ 2 + 2 * n + 1 := by linarith
        _ = (n + 1) ^ 2 := by ring
    done
  done

Verbatim from HTPILib/Chap6.lean (Velleman).

Three things worth naming.

ring, linarith and decide are standard Lean, not Velleman's dialect. They are the first genuine automation you meet, and they are the reason formalizing Chapter 6 is less tedious than formalizing Chapter 3.

Your turn

In Chap6Ex.lean, Section 6.1: 

theorem Exercise_6_1_9a : ∀ (n : Nat), 2 ∣ n ^ 2 + n := sorry

Verbatim from Chap6Ex.lean (Velleman).

This is Like_Example_6_1_2 with different numbers, so you can follow that proof structurally, line for line. Do it on paper first — in particular, work out the witness c before you type anything.

Then, harder and more interesting: 

theorem Like_Exercise_6_1_4 :
    ∀ (n : Nat), Sum i from 0 to n, 2 * i + 1 = (n + 1) ^ 2 := sorry

theorem Exercise_6_1_15 : ∀ n ≥ 10, 2 ^ n > n ^ 3 := sorry

Verbatim from Chap6Ex.lean (Velleman).

The first follows Like_Example_6_1_1; the second follows Example_6_1_3, and is a genuine fight, mostly because finding the right intermediate inequality is genuine work. That is fine. It is supposed to be.

A solution to 6.1.9(a), if you want to check yourself afterwards 
theorem Exercise_6_1_9a : ∀ (n : Nat), 2 ∣ n ^ 2 + n := by
  by_induc
  · -- Base Case
    define
    apply Exists.intro 0
    rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : 2 ∣ n ^ 2 + n
    define at ih
    obtain (k : Nat) (h1 : n ^ 2 + n = 2 * k) from ih
    define
    apply Exists.intro (k + n + 1)
    show (n + 1) ^ 2 + (n + 1) = 2 * (k + n + 1) from
      calc (n + 1) ^ 2 + (n + 1)
        _ = n ^ 2 + n + 2 * n + 2 := by ring
        _ = 2 * k + 2 * n + 2 := by rw [h1]
        _ = 2 * (k + n + 1) := by ring
    done
  done

Statement verbatim from Chap6Ex.lean; proof written for this page (not machine-checked). It is Like_Example_6_1_2 with the numbers changed — check it in Lean rather than believing this page.

Where to go after this

If you have got this far and want more, the natural next steps are Chapter 6's later sections — strong induction and recursion, where by_strong_induc and recursive definitions like fact and Fib live — and then Chapter 7, number theory, which is where the exercises stop feeling like exercises.

If instead you want to leave the dialect and use Lean for real mathematics, read the Transitioning to Standard Lean section of the appendix, then look at Mathlib. That is a different and much larger world, and nothing in this course is preparation for it beyond the one thing that matters: knowing what a goal state is and how to look at one.

Previous: Chapter 5 · The badge. · MATH 2055, Fall 2026. Taylor Dupuy, University of Vermont. Ungraded. Working through this page on your own is optional.