Proof: direct, contrapositive, contradiction and induction

Lens

MotivationH

Patterns that break

Mark points on a circle and join every pair of them by a straight chord, keeping the points in "general position" so that no three chords pass through one point. Count the regions into which the chords cut the disc.

points	1	2	3	4	5	6
regions	1	2	4	8	16	?

The pattern is irresistible: surely $6$ points give $32$ regions? They give 31.

Six points in general position on a circle and all fifteen chords between them. Count the regions carefully: there are 31, not 32.

The integers lesson met another trap: $n^2 + n + 41$ is prime for $n = 0, 1, \dots, 39$ and then fails. Examples can suggest a truth, and one counterexample can destroy a false one — but no number of examples can establish a statement about infinitely many cases. For that we need proof. This lesson is a toolkit of the four methods mathematicians use most, and a guide to spotting proofs that only look right.

IntuitionH

What a proof is

A proof is a finite chain of steps leading from accepted starting points — definitions, axioms and theorems already proved — to the statement we want. Each step must be justified: anyone who checks it should agree that it follows. A proof is not a feeling of certainty, and not a pile of examples; it is an argument that would convince a careful sceptic.

Most statements we prove have the shape "if $P$ then $Q$ ", possibly "for every $n$ ". The methods of this lesson are four ways of organising the chain, each resting on a law of logic from propositional logic:

Method	To prove	We assume	and derive	Logic behind it
direct	$P \to Q$	$P$	$Q$	the meaning of $\to$
cases	$P \to Q$ , when $P$ means " $A$ or $B$ "	$A$ , then separately $B$	$Q$ both times	$(A \to Q) \wedge (B \to Q) \equiv (A \vee B) \to Q$
contrapositive	$P \to Q$	$\neg Q$	$\neg P$	$P \to Q \equiv \neg Q \to \neg P$
contradiction	$S$	$\neg S$	something impossible	$(\neg S \to \bot) \to S$ is a tautology

The fourth row uses $\bot$ for "a contradiction", a statement that is certainly false, such as " $1 = 0$ " or " $q$ and not $q$ ". The fifth tool, induction, is different: it is a property of the natural numbers themselves, and it is how we prove infinitely many statements $P(0), P(1), P(2), \dots$ in one go.

DefinitionsH

Definitions we will use

Definition— even, odd, divides

An integer $n$ is even if $n = 2k$ for some integer $k$ , and odd if $n = 2k + 1$ for some integer $k$ . For integers $a$ and $b$ , $a$ divides $b$ , written $a \mid b$ , if $b = ak$ for some integer $k$ .

We use one fact about integers, which follows from division with remainder: every integer is either even or odd, and not both. (Dividing $n$ by $2$ leaves remainder $0$ or $1$ , and the remainder is unique.)

Definition— prime

A prime is a natural number $p > 1$ whose only positive divisors are $1$ and $p$ . Every natural number $n > 1$ has a smallest divisor $d > 1$ , and that $d$ is prime (a divisor of $d$ bigger than $1$ would be a smaller divisor of $n$ ).

Definition— induction

Ordinary induction. Let $P(n)$ be a statement about natural numbers $n = 0, 1, 2, \dots$ If

$P(0)$ is true (the base case), and
for every $n$ , $P(n)$ implies $P(n + 1)$ (the inductive step),

then $P(n)$ is true for every natural number $n$ . (To start at another number $n_0$ , take $n_0$ as the base case.)

Strong induction. If, for every $n$ , the truth of $P(k)$ for all $k < n$ implies $P(n)$ , then $P(n)$ is true for every $n$ .

The well-ordering principle. Every non-empty set of natural numbers has a least element.

ProofH

Direct proof and proof by cases

Theorem— Theorem 1

The sum of two odd integers is even.

Proof

Let $m$ and $n$ be odd. By definition $m = 2a + 1$ and $n = 2b + 1$ for some integers $a, b$ . Then

m + n = 2a + 2b + 2 = 2(a + b + 1),

and $a + b + 1$ is an integer, so $m + n$ is even.

∎

Notice the shape: unpack the definitions of the hypothesis, compute, and repack into the definition of the conclusion. Most direct proofs look like this.

Theorem— Theorem 2 (divisibility is transitive)

For integers $a, b, c$ : if $a \mid b$ and $b \mid c$ , then $a \mid c$ .

Proof

Since $a \mid b$ , there is an integer $k$ with $b = ak$ ; since $b \mid c$ , there is an integer $l$ with $c = bl$ . Then $c = (ak)l = a(kl)$ , and $kl$ is an integer, so $a \mid c$ .

∎

Theorem— Theorem 3 (proof by cases)

For every integer $n$ , the number $n(n + 1)$ is even.

Proof

Every integer is even or odd, so it is enough to treat the two cases.

Case 1: $n$ is even, say $n = 2k$ . Then $n(n + 1) = 2\,k(n + 1)$ , which is even.

Case 2: $n$ is odd, say $n = 2k + 1$ . Then $n + 1 = 2(k + 1)$ and $n(n + 1) = 2\,n(k + 1)$ , which is even.

∎

ProofH

Proof by contrapositive

Theorem— Theorem 4

Let $n$ be an integer. If $n^2$ is even, then $n$ is even.

A direct attempt stalls: from $n^2 = 2k$ we would want to "take square roots", and $\sqrt{2k}$ tells us nothing useful. The contrapositive is easy.

Proof

We prove the contrapositive: if $n$ is not even, then $n^2$ is not even. If $n$ is not even, it is odd, $n = 2k + 1$ . Then

n^2 = 4k^2 + 4k + 1 = 2(2k^2 + 2k) + 1,

which is odd, hence not even. Since a statement is equivalent to its contrapositive, the theorem is proved.

∎

Note

Be careful to prove the contrapositive $\neg Q \to \neg P$ and not the converse $Q \to P$ . "If $n$ is even then $n^2$ is even" is true and easy — but it is a different theorem.

ProofH

Proof by contradiction

To prove $S$ by contradiction, assume $\neg S$ and reason until you reach something impossible. Since true assumptions cannot lead to a false conclusion by valid steps, the assumption $\neg S$ must be false — so $S$ is true.

Theorem— Theorem 5 (Euclid)

There are infinitely many prime numbers.

Proof

Suppose, for a contradiction, that there are only finitely many primes, and list them all: $p_1, p_2, \dots, p_k$ . Let

N = p_1 p_2 \cdots p_k + 1 .

Then $N > 1$ , so $N$ has a smallest divisor $q > 1$ , and $q$ is prime. Since our list contains every prime, $q = p_i$ for some $i$ . But then $q$ divides the product $p_1 \cdots p_k$ and also $N$ , so it divides their difference $N - p_1 \cdots p_k = 1$ . No prime divides $1$ . This contradiction shows that the assumption was false: there are infinitely many primes.

∎

Note

The proof shows more: any finite list of primes misses the prime $q$ . Euclid himself (Elements, Book IX, Proposition 20) argued this way — "prime numbers are more than any assigned multitude of primes" — so the contradiction is optional. Notice also what the proof does not say: $N$ itself need not be prime. For the first six primes, $2 \cdot 3 \cdot 5 \cdot 7 \cdot 11 \cdot 13 + 1 = 30031 = 59 \cdot 509$ .

Theorem— Theorem 6

$\sqrt{2}$ is irrational: there are no integers $a, b$ with $b \neq 0$ and $(a/b)^2 = 2$ .

Proof

Suppose there were. Cancelling common factors, we may assume $a$ and $b$ are not both even. From $a^2 = 2b^2$ , $a^2$ is even, so $a$ is even by Theorem 4: $a = 2c$ . Then $4c^2 = 2b^2$ , so $b^2 = 2c^2$ is even, and $b$ is even by Theorem 4 again. Now $a$ and $b$ are both even — a contradiction.

∎

This classic chains two methods: a contradiction whose key step is the contrapositive Theorem 4. More on irrational numbers in real numbers.

ProofH

Induction

Picture an infinite row of dominoes. If the first falls, and each falling domino knocks over the next, then all of them fall. The base case pushes the first domino; the inductive step guarantees the chain reaction.

Theorem— Theorem 7 (Gauss's formula)

For every natural number $n$ : $\;0 + 1 + 2 + \dots + n = \dfrac{n(n + 1)}{2}$ .

Proof

Let $P(n)$ be the statement $0 + 1 + \dots + n = n(n+1)/2$ .

Base case. $P(0)$ says $0 = 0 \cdot 1/2$ , which is true.

Inductive step. Let $n$ be a natural number and assume $P(n)$ (the induction hypothesis). Then

0 + 1 + \dots + n + (n + 1) = \frac{n(n + 1)}{2} + (n + 1) = \frac{(n + 1)(n + 2)}{2},

which is $P(n + 1)$ . By induction, $P(n)$ holds for every $n$ .

∎

A proof without words of Gauss's formula for n = 4: two staircases of 1 + 2 + 3 + 4 squares fill a 4 by 5 rectangle, so 1 + 2 + 3 + 4 = (4 × 5) / 2.

A much-retold story has the young Carl Friedrich Gauss adding $1 + 2 + \dots + 100$ in moments by pairing $1 + 100$ , $2 + 99$ , …, fifty pairs of $101$ . The details of the story are uncertain, but the pairing idea is the picture above.

Theorem— Theorem 8

For every natural number $n$ : $\;1 + 3 + 5 + \dots + (2n - 1) = n^2$ .

Proof

Base case $n = 0$ : the empty sum is $0 = 0^2$ . Inductive step: if the first $n$ odd numbers add up to $n^2$ , then the first $n + 1$ add up to $n^2 + (2n + 1) = (n + 1)^2$ .

∎

Why the base case matters. Consider the claim " $n^2 + n + 1$ is even for every $n$ ". The inductive step works perfectly: $(n+1)^2 + (n+1) + 1 = (n^2 + n + 1) + 2(n + 1)$ , so if $n^2 + n + 1$ were even, the next value would be even too. But the base case fails — $0^2 + 0 + 1 = 1$ is odd — and in fact, by Theorem 3, $n^2 + n = n(n+1)$ is always even, so $n^2 + n + 1$ is never even. The dominoes are lined up beautifully; nobody pushed the first one.

Strong induction lets the inductive step use all earlier cases, not just the previous one.

Theorem— Theorem 9 (stamps)

With stamps worth $3$ and $5$ (in any currency), every amount of at least $8$ can be made exactly.

Proof

Let $P(n)$ be " $n = 3a + 5b$ for some natural numbers $a, b$ ". We prove $P(n)$ for every $n \ge 8$ by strong induction. The amounts $8 = 3 + 5$ , $9 = 3 + 3 + 3$ and $10 = 5 + 5$ can be made. Now let $n \ge 11$ and assume $P(k)$ for every $k$ with $8 \le k < n$ . Since $n - 3 \ge 8$ , the amount $n - 3$ can be made, $n - 3 = 3a + 5b$ ; adding one more $3$ gives $n = 3(a + 1) + 5b$ .

∎

The step reaches back three places, which is why we needed three starting cases. Strong induction also proves that every natural number $n > 1$ is a product of primes: either $n$ is prime, or $n = ab$ with $1 < a, b < n$ , and $a$ and $b$ are products of primes by the induction hypothesis — the existence half of the fundamental theorem of arithmetic.

Theorem— Theorem 10 (three equivalent principles)

Given the basic arithmetic of $\mathbb{N}$ , ordinary induction, strong induction and the well-ordering principle imply one another.

Proof

Ordinary ⇒ strong. Assume the hypothesis of strong induction for $P$ . Let $Q(n)$ be " $P(k)$ holds for every $k < n$ ". $Q(0)$ is true, since there is no $k < 0$ . If $Q(n)$ holds, then $P(n)$ holds by the hypothesis of strong induction, so $Q(n + 1)$ holds. By ordinary induction $Q(n)$ holds for every $n$ ; and $P(n)$ follows from $Q(n + 1)$ .

Strong ⇒ well-ordering. Let $S$ be a set of natural numbers with no least element; we show $S$ is empty. Let $P(n)$ be " $n \notin S$ ". If $P(k)$ holds for all $k < n$ , then $n \notin S$ — otherwise $n$ would be the least element of $S$ . By strong induction, no $n$ is in $S$ . So every non-empty set has a least element.

Well-ordering ⇒ ordinary. Suppose $P(0)$ holds and $P(n) \to P(n + 1)$ for every $n$ , but $P$ fails somewhere. Let $m$ be the least $n$ for which $P(n)$ fails. Then $m \neq 0$ , so $m = j + 1$ ; since $j < m$ , $P(j)$ holds, and therefore $P(j + 1) = P(m)$ holds — a contradiction.

∎

Explore

Explore: the logic behind the methods

Each method rests on a tautology. Check them in the truth-table explorer.

Why proof by contradiction works

If not-s leads to a contradiction (q and not q), then s. Is this true in every row?

Formula

Read as: (¬s → (q ∧ ¬q)) → s

Use the symbols ¬ ∧ ∨ → ↔, the words not, and, or, implies, iff, or ASCII ~ & | -> <->. Variables are single lowercase letters. ¬ binds tightest, then ∧, ∨, →, ↔; p → q → r means p → (q → r).

Try:

Tautology — true in all 4 rows.

q	s	¬s	¬q	q ∧ ¬q	¬s → q ∧ ¬q	(¬s → q ∧ ¬q) → s
T	T	F	F	F	T	T
T	F	T	F	F	F	T
F	T	F	T	F	T	T
F	F	T	T	F	F	T

4 rows: one for every way of making the 2 variables true or false.

Things to try:

Change the formula to (p -> q) <-> (~q -> ~p) — the contrapositive method.
Try ((a -> q) and (b -> q)) <-> ((a or b) -> q) — proof by cases.
Try the mistaken method (p -> q) <-> (q -> p): proving the converse instead. Which row breaks it?

ExplanationH

Spot the error

Learning to find the flaw in a wrong proof is as important as writing a right one. Each of these "proofs" has exactly one fatal step. Try to find it before reading the diagnosis.

Example— All horses are the same colour

Claim: in every set of $n \ge 1$ horses, all the horses have the same colour. "Proof" by induction: one horse has the same colour as itself. Now take $n + 1$ horses. Remove one: the remaining $n$ have one colour, by the induction hypothesis. Put it back and remove a different one: again the remaining $n$ share one colour. The two groups overlap, so all $n + 1$ horses share a colour.

Diagnosis: the inductive step fails from $n = 1$ to $n = 2$ . With two horses, the two groups of size one do not overlap, so nothing connects their colours. An inductive step must work for every $n$ , including the smallest. (This puzzle is usually credited to George Pólya.)

Example— 2 = 1

"Proof": let $a = b$ . Then $a^2 = ab$ , so $a^2 - b^2 = ab - b^2$ , that is, $(a + b)(a - b) = b(a - b)$ . Cancelling, $a + b = b$ , so $2b = b$ and $2 = 1$ .

Diagnosis: "cancelling" divides by $a - b$ , which is $0$ . Hidden assumptions — here, that a number is non-zero — are the most common flaw in algebraic proofs.

Example— The largest natural number is 1

"Proof": let $N$ be the largest natural number. Since $N^2 \ge N$ and $N$ is the largest, $N^2 = N$ , so $N = 0$ or $N = 1$ ; and $1 > 0$ , so $N = 1$ .

Diagnosis: the first sentence assumes, without justification, that a largest natural number exists. Every step after that is correct — which shows only that the assumption is false. (This is known as Perron's paradox.) A contradiction blames some assumption; make sure it is the one you meant to refute.

Example— A circular proof

Claim: if $n^2$ is even then $n$ is even. "Proof": let $n$ be even, $n = 2k$ ; then $n^2 = 4k^2 = 2(2k^2)$ is even.

Diagnosis: this proves the converse. It assumes the conclusion (" $n$ is even") and derives the hypothesis. Compare it with the proof of Theorem 4.

Formal mathematicsF

The proofs, checked by Lean

Every theorem of this lesson is proved in Lean below, almost always in the same way as in the text. Direct proofs unpack definitions with obtain and repack them; ring does the algebra.

odd_add_oddLean 4Proved here from basic factsFormally verified

/-- **Direct proof.** The sum of two odd integers is even: if `m = 2a + 1` and `n = 2b + 1`, then
`m + n = 2(a + b + 1)`. (Mathlib's `Even k` means `k = r + r` for some `r`.) -/
theorem odd_add_odd {m n : ℤ} (hm : Odd m) (hn : Odd n) : Even (m + n) := by
  obtain ⟨a, rfl⟩ := hm
  obtain ⟨b, rfl⟩ := hn
  exact ⟨a + b + 1, by ring⟩

Axioms used: propextformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

dvd_transLean 4Proved here from basic factsFormally verified

/-- **Direct proof.** Divisibility is transitive: if `b = a·k` and `c = b·l` then `c = a·(k·l)`. -/
theorem dvd_trans {a b c : ℤ} (hab : a ∣ b) (hbc : b ∣ c) : a ∣ c := by
  obtain ⟨k, rfl⟩ := hab
  obtain ⟨l, rfl⟩ := hbc
  exact ⟨k * l, by ring⟩

Axioms used: propextformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

even_mul_succLean 4Proved here from basic factsFormally verified

/-- **Proof by cases.** For every integer `n`, the product `n(n + 1)` is even.
Case 1: `n = 2k` is even, so `n(n + 1) = 2·(k(n + 1))`.
Case 2: `n = 2k + 1` is odd, so `n + 1 = 2(k + 1)` and `n(n + 1) = 2·(n(k + 1))`. -/
theorem even_mul_succ (n : ℤ) : Even (n * (n + 1)) := by
  rcases Int.even_or_odd n with ⟨k, hk⟩ | ⟨k, hk⟩
  · exact ⟨k * (n + 1), by rw [hk]; ring⟩
  · exact ⟨n * (k + 1), by rw [hk]; ring⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

The contrapositive proof uses by_contra: assume n is not even and derive a contradiction with the hypothesis. Mathlib proves the same fact as part of a general lemma about powers.

odd_sq_of_oddLean 4Proved here from basic factsFormally verified

/-- The square of an odd integer is odd: `(2k + 1)² = 2(2k² + 2k) + 1`. -/
theorem odd_sq_of_odd {n : ℤ} (h : Odd n) : Odd (n ^ 2) := by
  obtain ⟨k, rfl⟩ := h
  exact ⟨2 * k ^ 2 + 2 * k, by ring⟩

Axioms used: propextformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

even_of_even_sqLean 4Proved here from basic factsFormally verified

/-- **Proof by contrapositive.** If `n²` is even, then `n` is even. We prove the contrapositive
instead: if `n` is not even, it is odd, so `n²` is odd (`odd_sq_of_odd`), hence not even. -/
theorem even_of_even_sq (n : ℤ) (h : Even (n ^ 2)) : Even n := by
  by_contra hn
  have hodd : Odd (n ^ 2) := odd_sq_of_odd (Int.not_even_iff_odd.mp hn)
  exact (Int.not_even_iff_odd.mpr hodd) h

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

even_of_even_sq_libraryLean 4Applies a library theoremFormally verified

/-- The same theorem from Mathlib's `Int.even_pow : Even (m ^ n) ↔ Even m ∧ n ≠ 0`. -/
theorem even_of_even_sq_library (n : ℤ) (h : Even (n ^ 2)) : Even n :=
  (Int.even_pow.mp h).1

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

Euclid's theorem in the "every finite list misses a prime" form. Nat.minFac N is the smallest factor of N bigger than 1.

exists_prime_not_memLean 4Proved here from basic factsFormally verified

/-- **Euclid's theorem.** Every finite set `S` of primes misses some prime.
Let `N = (∏ p ∈ S, p) + 1` and let `q` be the smallest factor of `N` that is bigger than `1`
(it is prime). If `q` were in `S`, it would divide both the product and `N`, hence their
difference `1` — a contradiction. Note that `N` itself need not be prime. -/
theorem exists_prime_not_mem (S : Finset ℕ) (hS : ∀ p ∈ S, p.Prime) :
    ∃ q, q.Prime ∧ q ∉ S := by
  have hpos : 0 < ∏ p ∈ S, p := Finset.prod_pos fun p hp => (hS p hp).pos
  have hN : (∏ p ∈ S, p) + 1 ≠ 1 := by omega
  refine ⟨Nat.minFac ((∏ p ∈ S, p) + 1), Nat.minFac_prime hN, fun hmem => ?_⟩
  have hdvd_prod : Nat.minFac ((∏ p ∈ S, p) + 1) ∣ ∏ p ∈ S, p := Finset.dvd_prod_of_mem _ hmem
  have hdvd_N := Nat.minFac_dvd ((∏ p ∈ S, p) + 1)
  have hdvd_one : Nat.minFac ((∏ p ∈ S, p) + 1) ∣ 1 := (Nat.dvd_add_right hdvd_prod).mp hdvd_N
  exact (Nat.minFac_prime hN).one_lt.ne' (Nat.dvd_one.mp hdvd_one)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

exists_infinite_primesLean 4Applies a library theoremFormally verified

/-- There are primes as large as we like: Mathlib's `Nat.exists_infinite_primes`, proved with
the smallest prime factor of `n! + 1`. -/
theorem exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ p.Prime :=
  Nat.exists_infinite_primes n

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

For $\sqrt{2}$ the Lean proof avoids "cancel common factors" and uses infinite descent instead: a solution of $a^2 = 2b^2$ with $b \neq 0$ would produce a smaller one, $c^2 = 2d^2$ with $a = 2c$ and $b = 2d$ , and that is impossible by strong induction. (Pierre de Fermat made this method famous in the 17th century.)

sq_eq_two_mul_sqLean 4Proved here from basic factsFormally verified

/-- **√2 is irrational**, in the form: if `a² = 2b²` for natural numbers `a, b`, then `b = 0`.
Proof by *infinite descent* (strong induction on `b`): `a²` is even, so `a = 2c`; then `b² = 2c²`,
so `b = 2d`; then `c² = 2d²` is a smaller solution, and by the induction hypothesis `d = 0`, so
`b = 0`. (Evenness of a square is Mathlib's `Nat.even_pow`; the lesson proves it as Theorem 4.) -/
theorem sq_eq_two_mul_sq (a b : ℕ) (h : a ^ 2 = 2 * b ^ 2) : b = 0 := by
  induction b using Nat.strong_induction_on generalizing a with
  | _ b ih =>
    have ha : Even a := (Nat.even_pow.mp ⟨b ^ 2, by rw [h]; ring⟩).1
    obtain ⟨c, rfl⟩ := ha
    have hb2 : b ^ 2 = 2 * c ^ 2 := by nlinarith
    have hb : Even b := (Nat.even_pow.mp ⟨c ^ 2, by rw [hb2]; ring⟩).1
    obtain ⟨d, rfl⟩ := hb
    have hc : c ^ 2 = 2 * d ^ 2 := by nlinarith
    by_contra hne
    have hd : d = 0 := ih d (by omega) c hc
    omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

Induction proofs use induction n with | zero => … | succ n ih => …, where ih is the induction hypothesis. To avoid fractions, Gauss's formula is stated as $2(0 + 1 + \dots + n) = n(n + 1)$ ; the calc block follows the human proof line by line.

gauss_sumLean 4Proved here from basic factsFormally verified

/-- **Gauss's formula, by induction:** `2·(0 + 1 + ⋯ + n) = n(n + 1)`.
Base case: both sides are `0`. Inductive step: if `2·(0 + ⋯ + n) = n(n + 1)`, then
`2·(0 + ⋯ + n + (n + 1)) = n(n + 1) + 2(n + 1) = (n + 1)(n + 2)`. -/
theorem gauss_sum (n : ℕ) : 2 * ∑ i ∈ range (n + 1), i = n * (n + 1) := by
  induction n with
  | zero => rfl
  | succ n ih =>
    calc 2 * ∑ i ∈ range (n + 1 + 1), i
        = 2 * ∑ i ∈ range (n + 1), i + 2 * (n + 1) := by rw [sum_range_succ, mul_add]
      _ = n * (n + 1) + 2 * (n + 1) := by rw [ih]
      _ = (n + 1) * (n + 1 + 1) := by ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

gauss_sum_libraryLean 4Applies a library theoremFormally verified

/-- Mathlib's version, `Finset.sum_range_id_mul_two : (∑ i ∈ range n, i) * 2 = n * (n - 1)`. -/
theorem gauss_sum_library (n : ℕ) : (∑ i ∈ range n, i) * 2 = n * (n - 1) :=
  sum_range_id_mul_two n

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

sum_oddLean 4Proved here from basic factsFormally verified

/-- **The odd numbers add up to squares:** `1 + 3 + ⋯ + (2n − 1) = n²`, by induction.
The inductive step is `n² + (2n + 1) = (n + 1)²`. -/
theorem sum_odd (n : ℕ) : ∑ i ∈ range n, (2 * i + 1) = n ^ 2 := by
  induction n with
  | zero => rfl
  | succ n ih => rw [sum_range_succ, ih]; ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

stampsLean 4Proved here from basic factsFormally verified

/-- **Strong induction.** Every whole number `n ≥ 8` is a sum of 3s and 5s.
The cases `8 = 3 + 5`, `9 = 3 + 3 + 3` and `10 = 5 + 5` start things off; for `n ≥ 11` the
number `n − 3 ≥ 8` is smaller, so (strong induction hypothesis) it is `3a + 5b`, and then
`n = 3(a + 1) + 5b`. The step reaches back *three* places, which ordinary induction cannot do
directly. -/
theorem stamps (n : ℕ) (hn : 8 ≤ n) : ∃ a b : ℕ, n = 3 * a + 5 * b := by
  induction n using Nat.strong_induction_on with
  | _ n ih =>
    rcases (show n = 8 ∨ n = 9 ∨ n = 10 ∨ 11 ≤ n by omega) with h | h | h | h
    · exact ⟨1, 1, by omega⟩
    · exact ⟨3, 0, by omega⟩
    · exact ⟨0, 2, by omega⟩
    · obtain ⟨a, b, hab⟩ := ih (n - 3) (by omega) (by omega)
      exact ⟨a + 1, b, by omega⟩

Axioms used: propext, Quot.soundformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

The fake theorem: Lean happily proves the inductive step — and also proves that the statement is false for every $n$ .

false_step_holdsLean 4Proved here from basic factsFormally verified

/-- A **fake induction**: *if* `n² + n + 1` were even, *then* `(n + 1)² + (n + 1) + 1` would be
even too, because the second number is the first plus `2(n + 1)`. The inductive step is fine… -/
theorem false_step_holds (n : ℕ) (h : Even (n ^ 2 + n + 1)) :
    Even ((n + 1) ^ 2 + (n + 1) + 1) := by
  have e : (n + 1) ^ 2 + (n + 1) + 1 = (n ^ 2 + n + 1) + 2 * (n + 1) := by ring
  rw [e]
  exact h.add (even_two_mul (n + 1))

Axioms used: propextformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

never_evenLean 4Proved here from basic factsFormally verified

/-- …but the base case fails, and in fact the claim is false for **every** `n`: `n² + n = n(n + 1)`
is even (it is a product of consecutive numbers), so `n² + n + 1` is odd. -/
theorem never_even (n : ℕ) : ¬ Even (n ^ 2 + n + 1) := by
  have h : Even (n * (n + 1)) := Nat.even_mul_succ_self n
  have e : n ^ 2 + n + 1 = n * (n + 1) + 1 := by ring
  rw [e, Nat.even_add_one]
  exact not_not.mpr h

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

OrdinaryInductionLean 4Formally verified

/-- The principle of **ordinary induction** for `ℕ`, stated as a proposition. -/
def OrdinaryInduction : Prop :=
  ∀ P : ℕ → Prop, P 0 → (∀ n, P n → P (n + 1)) → ∀ n, P n

Axioms used: No axiomsformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

StrongInductionLean 4Formally verified

/-- The principle of **strong induction**: if `P n` follows whenever `P k` holds for all `k < n`,
then `P n` holds for every `n`. (No separate base case: for `n = 0` there are no `k < 0`.) -/
def StrongInduction : Prop :=
  ∀ P : ℕ → Prop, (∀ n, (∀ k < n, P k) → P n) → ∀ n, P n

Axioms used: No axiomsformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

WellOrderingLean 4Formally verified

/-- The **well-ordering principle**: every non-empty set of natural numbers has a least element. -/
def WellOrdering : Prop :=
  ∀ S : Set ℕ, S.Nonempty → ∃ m ∈ S, ∀ k ∈ S, m ≤ k

Axioms used: No axiomsformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

ordinaryInduction_holdsLean 4Applies a library theoremFormally verified

/-- Ordinary induction holds: it is the recursor `Nat.rec` that comes with the definition of `ℕ`. -/
theorem ordinaryInduction_holds : OrdinaryInduction :=
  fun _ h0 hs n => Nat.rec h0 hs n

Axioms used: No axiomsformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

strong_of_ordinaryLean 4Proved here from basic factsFormally verified

/-- **Ordinary ⇒ strong induction.** Apply ordinary induction to the stronger statement
`Q n := ∀ k < n, P k`. `Q 0` is vacuous; and if `Q n` holds then `P n` holds by the hypothesis,
so `Q (n + 1)` holds. Finally `P n` follows from `Q (n + 1)`.
(All three principles are theorems about `ℕ` in Lean; what these proofs show is that each one can
be *derived* from the previous one, using only basic arithmetic facts.) -/
theorem strong_of_ordinary (ind : OrdinaryInduction) : StrongInduction := by
  intro P h n
  have hQ : ∀ m, ∀ k < m, P k := by
    refine ind (fun m => ∀ k < m, P k) (fun k hk => absurd hk (Nat.not_lt_zero k)) ?_
    intro m hm k hk
    rcases Nat.lt_succ_iff_lt_or_eq.mp hk with hlt | heq
    · exact hm k hlt
    · rw [heq]; exact h m hm
  exact hQ (n + 1) n (Nat.lt_succ_self n)

Axioms used: No axiomsformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

wellOrdering_of_strongLean 4Proved here from basic factsFormally verified

/-- **Strong induction ⇒ well-ordering.** Suppose `S` had no least element. By strong induction,
no `n` is in `S`: if all `k < n` are outside `S` and `n ∈ S`, then `n` would be the least element.
So `S` is empty, contradicting the hypothesis. -/
theorem wellOrdering_of_strong (sind : StrongInduction) : WellOrdering := by
  intro S hne
  by_contra hno
  push Not at hno
  have hout : ∀ n, n ∉ S := by
    refine sind (fun n => n ∉ S) ?_
    intro n ih hn
    obtain ⟨k, hkS, hkn⟩ := hno n hn
    exact ih k hkn hkS
  obtain ⟨x, hx⟩ := hne
  exact hout x hx

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

ordinary_of_wellOrderingLean 4Proved here from basic factsFormally verified

/-- **Well-ordering ⇒ ordinary induction.** If `P 0` and `P n → P (n + 1)`, but `P` failed
somewhere, let `m` be the *least* failure. `m ≠ 0` because `P 0` holds, so `m = j + 1`; and `j < m`
means `P j` holds, hence `P (j + 1) = P m` holds — a contradiction. -/
theorem ordinary_of_wellOrdering (wo : WellOrdering) : OrdinaryInduction := by
  intro P h0 hs n
  by_contra hn
  obtain ⟨m, hm, hmin⟩ := wo {k | ¬ P k} ⟨n, hn⟩
  cases m with
  | zero => exact hm h0
  | succ j =>
    have hj : P j := by
      by_contra hj
      have := hmin j hj
      omega
    exact hm (hs j hj)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ProofTechniques.leanTry it in the Lean web editor

A subtle point: all three principles are theorems about $\mathbb{N}$ in Lean, so the implications between them could be proved trivially by ignoring the hypothesis. What makes these proofs meaningful is that they do not: each uses only its hypothesis and elementary arithmetic, exactly as in Theorem 10.

ComputationC

Evidence, counterexamples and proof

Regions of a circle: a pattern that breaksPythonExact computationCounterexampleComputationally tested

"""Circle regions: a pattern that breaks.

Put n points on a circle and draw every chord between them. How many regions
does the disc fall into? For n = 1, 2, 3, 4, 5 the answers are 1, 2, 4, 8, 16,
which suggests 2**(n - 1). For n = 6 the answer is 31.

We count regions exactly. The points are rational points of the unit circle,
((1 - t^2)/(1 + t^2), 2t/(1 + t^2)), so every chord crossing is computed with
exact fractions. The chords cut the disc into a connected plane graph, and
Euler's formula V - E + F = 2 then gives

    regions = 1 + (number of chords) + sum over crossing points P of (m_P - 1),

where m_P is the number of chords through P. (Each chord adds one region, and
each crossing on it adds one more.) If no three chords meet at a point this is
1 + C(n, 2) + C(n, 4), which is not a power of 2 for n = 6. If three chords
do meet - as the three diameters of a symmetric hexagon do - the count drops.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

from fractions import Fraction
from itertools import combinations
from math import comb

def circle_point(t):
    """The rational point of the unit circle with parameter t (a Fraction)."""
    t = Fraction(t)
    d = 1 + t * t
    return ((1 - t * t) / d, 2 * t / d)

def crossing(a, b, c, d):
    """The point where chords ab and cd cross strictly inside both, or None."""
    (x1, y1), (x2, y2), (x3, y3), (x4, y4) = a, b, c, d
    den = (x2 - x1) * (y4 - y3) - (y2 - y1) * (x4 - x3)
    if den == 0:
        return None
    s = ((x3 - x1) * (y4 - y3) - (y3 - y1) * (x4 - x3)) / den
    u = ((x3 - x1) * (y2 - y1) - (y3 - y1) * (x2 - x1)) / den
    if 0 < s < 1 and 0 < u < 1:
        return (x1 + s * (x2 - x1), y1 + s * (y2 - y1))
    return None

def regions(points):
    """Number of regions into which all chords between ``points`` cut the disc."""
    chords = list(combinations(points, 2))
    through = {}
    for (i, ch1), (j, ch2) in combinations(enumerate(chords), 2):
        if set(ch1) & set(ch2):
            continue                        # chords sharing an endpoint
        p = crossing(*ch1, *ch2)
        if p is not None:
            through.setdefault(p, set()).update((i, j))
    return 1 + len(chords) + sum(len(s) - 1 for s in through.values())

def general_position_formula(n):
    """1 + C(n, 2) + C(n, 4): the count when no three chords are concurrent."""
    return 1 + comb(n, 2) + comb(n, 4)

#: Parameters giving points in general position for n <= 8.
PARAMS = [Fraction(k, 7) for k in (0, 2, 5, 9, 14, 22, 37, 61)]

#: Three antipodal pairs: the three diameters all pass through the centre.
HEXAGON_WITH_DIAMETERS = [(Fraction(1), Fraction(0)), (Fraction(-1), Fraction(0)),
                          (Fraction(3, 5), Fraction(4, 5)),
                          (Fraction(-3, 5), Fraction(-4, 5)),
                          (Fraction(-3, 5), Fraction(4, 5)),
                          (Fraction(3, 5), Fraction(-4, 5))]

def main():
    print(" n  regions  2^(n-1)  1+C(n,2)+C(n,4)")
    for n in range(1, 9):
        r = regions([circle_point(t) for t in PARAMS[:n]])
        guess = 2 ** (n - 1)
        mark = "" if r == guess else "   <- pattern broken"
        print(f"{n:2d}  {r:7d}  {guess:7d}  {general_position_formula(n):15d}{mark}")
    print()
    r6 = regions(HEXAGON_WITH_DIAMETERS)
    print(f"Six points forming three diameters (concurrent at the centre): {r6}")
    print("The count depends on the positions, not only on n.")
    print()
    print("Epistemic status: exact counts for these particular point sets, using")
    print("rational arithmetic and Euler's formula (a theorem). They refute the")
    print("guess 2^(n-1): one counterexample suffices. The general formula for")
    print("points in general position needs a proof; numbers cannot supply it.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The counts $1, 2, 4, 8, 16$ really do continue $31, 57, 99$ : the general formula for points in general position is $1 + \binom{n}{2} + \binom{n}{4}$ , which a counting argument (with Euler's formula $V - E + F = 2$ ) proves. And when three chords meet at one point the count drops — so even "the number of regions for $n$ points" needs the hypothesis of general position.

Euclid's numbers and induction formulas, checkedPythonExact computationExhaustive finite checkComputationally tested

"""Euclid's numbers, and evidence versus proof for induction formulas.

Euclid's proof that there are infinitely many primes multiplies the primes of
a finite list and adds 1. The result N need not be prime itself - but every
prime factor of N is missing from the list. Here we factor N for the lists of
the first k primes, k = 1, ..., 9, and check that each factor is new.

Then we test two formulas proved by induction in the lesson,
1 + 2 + ... + n = n(n + 1)/2 and 1 + 3 + ... + (2n - 1) = n^2, for every n up
to 10 000, and a false claim whose inductive step works but whose base case
fails: "n^2 + n + 1 is even".

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

from math import prod

def first_primes(k):
    """The first k primes."""
    primes = []
    n = 2
    while len(primes) < k:
        if all(n % p for p in primes if p * p <= n):
            primes.append(n)
        n += 1
    return primes

def factorize(n):
    """Prime factorisation of n >= 2 by trial division, as a sorted list."""
    if n < 2:
        raise ValueError("n must be at least 2")
    factors = []
    d = 2
    while d * d <= n:
        while n % d == 0:
            factors.append(d)
            n //= d
        d += 1
    if n > 1:
        factors.append(n)
    return factors

def euclid_number(primes):
    """The product of the given primes, plus one."""
    return prod(primes) + 1

def first_failure(claim, upto):
    """The least n in 0..upto with claim(n) false, or None."""
    for n in range(upto + 1):
        if not claim(n):
            return n
    return None

def step_difference(n):
    """(n+1)^2 + (n+1) + 1 minus n^2 + n + 1: always 2(n + 1), an even number,
    which is why "n^2 + n + 1 even" would pass from n to n + 1."""
    return ((n + 1) ** 2 + (n + 1) + 1) - (n * n + n + 1)

def running_check(term, closed_form, upto):
    """Check sum_{i < n} term(i) == closed_form(n) for n = 0..upto,
    accumulating the sum; return the first n where it fails, or None."""
    total = 0
    for n in range(upto + 1):
        if total != closed_form(n):
            return n
        total += term(n)
    return None

def main():
    print(" k  2*3*...*p_k + 1   factorisation           all factors new?")
    for k in range(1, 10):
        ps = first_primes(k)
        n = euclid_number(ps)
        fs = factorize(n)
        shown = " * ".join(map(str, fs)) if len(fs) > 1 else "prime"
        new = all(f not in ps for f in fs)
        print(f"{k:2d}  {n:15d}   {shown:22}  {'yes' if new else 'NO'}")
    print()
    upto = 10_000
    g = running_check(lambda i: i, lambda n: n * (n - 1) // 2, upto)
    o = running_check(lambda i: 2 * i + 1, lambda n: n * n, upto)
    print(f"Gauss: 0+1+...+(n-1) = n(n-1)/2, n <= {upto}: "
          f"{'no failure' if g is None else g}")
    print(f"Odd numbers: 1+3+...+(2n-1) = n^2, n <= {upto}: "
          f"{'no failure' if o is None else o}")
    step = all(step_difference(n) == 2 * (n + 1) for n in range(upto + 1))
    base = first_failure(lambda n: (n * n + n + 1) % 2 == 0, upto)
    print("'n^2+n+1 is even': consecutive values differ by 2(n+1) for all")
    print(f"  n <= {upto}: {step}. So the inductive step works - yet the claim")
    print(f"  fails at n = {base}, the base case, and in fact at every n.")
    print()
    print("Epistemic status: exact arithmetic. The factorisations are complete")
    print("and show that Euclid's numbers need not be prime. The formula checks")
    print("cover n <= 10000 only - finite evidence. The induction proofs in the")
    print("lesson cover every n; the last line shows why a base case is needed.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The factorisations show every prime factor of $p_1 \cdots p_k + 1$ is new, as Euclid's proof guarantees — and that the number itself is often not prime. Checking Gauss's formula for $n \le 10\,000$ is reassuring but finite; the induction proof covers every $n$ at once.

Exercises

1. Proof: direct, contrapositive, contradiction and induction

Warm-upHuman

You want to prove “if $n^2$ is odd, then $n$ is odd” by contrapositive. What do you assume at the start?

Choose one

n

is even

n^2

is odd

n

is odd

n^2

is even

2. Proof: direct, contrapositive, contradiction and induction

Warm-upHuman

Use Gauss's formula to compute $1 + 2 + 3 + \dots + 200$ .

3. Proof: direct, contrapositive, contradiction and induction

CoreHuman

In the “all horses are the same colour” induction, where exactly does the argument break down?

Choose one

The base case: one horse need not have one colour.The inductive step from

n = 1

n = 2

: the two groups of size

1

do not overlap.The inductive step only fails for large

n

.Nothing is wrong; the induction principle itself is the problem.

4. Proof: direct, contrapositive, contradiction and induction

CoreHuman

Let $N = 2 \cdot 3 \cdot 5 \cdot 7 \cdot 11 \cdot 13 + 1 = 30031$ . What does Euclid's argument guarantee about $N$ ?

Choose one

Every prime factor of

N

is different from

2, 3, 5, 7, 11, 13

N

is prime.

N

's smallest prime factor is the next prime,

17

.Nothing: the argument only works when the list contains every prime.

5. Proof: direct, contrapositive, contradiction and induction

CoreHuman

With an unlimited supply of stamps worth $3$ and $7$ , what is the largest amount that cannot be made exactly?

6. Proof: direct, contrapositive, contradiction and induction

CoreHuman

Which of these statements is proved most naturally by strong induction rather than ordinary induction?

Choose one

Every natural number

n \ge 2

is a product of primes.

0 + 1 + \dots + n = n(n+1)/2

1 + 3 + \dots + (2n - 1) = n^2

2^n \ge n + 1

for every natural number

n

7. Proof: direct, contrapositive, contradiction and induction

CoreHuman

“Let $a = b$ . Then $a^2 = ab$ , so $a^2 - b^2 = ab - b^2$ , so $(a+b)(a-b) = b(a-b)$ , so $a + b = b$ , so $2b = b$ , so $2 = 1$ .” Which step is invalid?

Choose one

From

(a+b)(a-b) = b(a-b)

a + b = b

From

a = b

a^2 = ab

From

a^2 - b^2 = ab - b^2

(a+b)(a-b) = b(a-b)

From

2b = b

2 = 1

8. Proof: direct, contrapositive, contradiction and induction

StretchHuman

A student proves: “if $n^2 + n + 1$ is even, then $(n+1)^2 + (n+1) + 1$ is even”, and concludes by induction that $n^2 + n + 1$ is even for all $n$ . Which statement is correct?

Choose one

The inductive step is valid, but the base case fails, and in fact

n^2 + n + 1

is odd for every

n

.The proof is correct.The inductive step is wrong algebra.The claim is true from

n = 1

onwards; only

n = 0

fails.

9. Proof: direct, contrapositive, contradiction and induction

CoreFormal

Which Lean proposition expresses the principle of ordinary induction for the natural numbers?

Choose one

∀ P : ℕ → Prop, P 0 → (∀ n, P n → P (n + 1)) → ∀ n, P n∀ P : ℕ → Prop, (∀ n, P n → P (n + 1)) → ∀ n, P n∀ P : ℕ → Prop, P 0 → ∀ n, P n∀ P : ℕ → Prop, (∀ n, P n) → P 0 ∧ ∀ n, P n → P (n + 1)

10. Proof: direct, contrapositive, contradiction and induction

StretchComputational

Write is_prime(n) and first_failure(claim, limit), which returns the least n with 0 <= n <= limit for which claim(n) is false, or None if there is none. Use them to find the first n for which $n^2 + n + 41$ is not prime. Why does your search not prove anything about the values beyond limit?

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"I checked it for many numbers, so it is proved." Examples are evidence, not proof. The circle regions agree with $2^{n-1}$ five times and then fail; $n^2 + n + 41$ is prime forty times and then fails.

Misconception

Proving the converse instead of the statement. To prove "if $n^2$ is even then $n$ is even" you must start from " $n^2$ is even" (or, by contrapositive, from " $n$ is odd"). Starting from " $n$ is even" proves a different theorem.

Misconception

"The inductive step is the real work, so the base case can be skipped." Without a base case an induction proves nothing: " $n^2 + n + 1$ is even" has a valid inductive step and is false for every $n$ .

Misconception

Assuming what is to be proved. A proof that uses its conclusion as a step — perhaps hidden in a phrase like "clearly" or in a diagram — is circular, however long it is.

Misconception

Blaming the wrong assumption. A contradiction shows that at least one of your assumptions is false. If you made an extra, unjustified assumption along the way ("let $N$ be the largest natural number"), the contradiction may be its fault, not the fault of the hypothesis you meant to refute.

Misconception

"Euclid's proof shows that $p_1 p_2 \cdots p_k + 1$ is prime." It shows only that its prime factors are new. $2 \cdot 3 \cdot 5 \cdot 7 \cdot 11 \cdot 13 + 1 = 59 \cdot 509$ .

ViewpointsH

Many ways of seeing

Logic— proofs as mathematical objects

Logicians study proofs themselves. In a formal system a proof is a finite object — a list or tree of formulas, each an axiom or obtained from earlier ones by a rule — and checking it is mechanical, as Lean does. Gerhard Gentzen's work in the 1930s made the structure of proofs a subject of its own; see proof theory. Logic also distinguishes our methods sharply: proving $\neg P$ by assuming $P$ and deriving a contradiction is fine in every logic, but proving $P$ by refuting $\neg P$ uses the law of excluded middle, which constructive mathematicians do not assume. Euclid's theorem survives either way, because his argument actually constructs a new prime.

Computation— induction is recursion

A proof by induction is a recipe: to get $P(5)$ , start from $P(0)$ and apply the inductive step five times. Under the propositions-as-types correspondence this is literally a recursive program, and in Lean the proof of gauss_sum is a recursive function on natural numbers. Programmers use the same idea to prove loops correct: a loop invariant is a statement true before the first iteration (base case) and preserved by each iteration (inductive step). See algorithms, correctness and efficiency.

Combinatorics— proof by counting

A different kind of proof of Gauss's formula counts one set in two ways. How many ways are there to choose two different numbers from $\{0, 1, \dots, n\}$ ? Choosing the larger one first: if it is $j$ , there are $j$ choices for the smaller, giving $0 + 1 + \dots + n$ . On the other hand the number of pairs from $n + 1$ objects is $\binom{n+1}{2} = \frac{(n+1)n}{2}$ . Such double counting arguments often explain a formula better than an induction, which verifies it.

Geometry— proofs without words

The staircase picture proves Gauss's formula for every $n$ at once, if one reads it as a general construction. The odd-number formula has a picture too: an $n \times n$ square grows into an $(n+1) \times (n+1)$ square by adding an L-shaped border of $2n + 1$ squares — the shape the Pythagoreans called a gnomon. Pictures can mislead (the circle regions!), so a picture becomes a proof only when we can say precisely why it works for every case.

History & global context

History and global context

Euclid's Elements (Alexandria, around 300 BCE) organised geometry and number theory as a chain of propositions deduced from definitions and postulates — the model of mathematical proof for two thousand years. Book IX, Proposition 20 is the infinitude of primes; Book VII contains the theory of divisibility used in our next number-theory lesson.
China. In his commentary (263 CE) on The Nine Chapters on the Mathematical Art, Liu Hui justified the book's procedures with careful arguments, for example dissection proofs of area and volume formulas.
India. The Yuktibhāṣā of Jyeṣṭhadeva (Kerala, around 1530) explains in detail the reasons (yukti) behind the infinite series of Mādhava's school, including arguments that proceed step by step through all whole numbers.
Early induction. Around 1000 CE al-Karajī in Baghdad gave arguments about sums of cubes and binomial coefficients that pass from each case to the next, which historians see as an early form of induction; Levi ben Gershon (Gersonides, 1321), Francesco Maurolico (1575) and Blaise Pascal (1654) used the method more explicitly. The name "mathematical induction" was popularised by Augustus De Morgan in 1838.
Foundations. Richard Dedekind (1888) and Giuseppe Peano (1889) made induction one of the defining properties of the natural numbers.

Patterns that break

What a proof is

Definitions we will use

Direct proof and proof by cases

Proof by contrapositive

Proof by contradiction

Induction

Explore: the logic behind the methods

Spot the error

The proofs, checked by Lean

Evidence, counterexamples and proof

Exercises

Common misconceptions

Many ways of seeing

History and global context

Further reading