---
title: Proof Techniques
module: Foundations
moduleNumber: 1
lessonNumber: 2
order: 102
summary: |
  An algorithm without a proof is a conjecture. This lesson collects the handful
  of arguments that certify the algorithms in this course — direct proof,
  contrapositive, contradiction, ordinary and strong induction, construction, and
  disproof by counterexample — each with a small worked
  example and a picture. Loop invariants are a form of induction,
  recursive correctness falls to strong induction, and the classic broken proofs
  (all horses are the same color) show where inductions go wrong.
topics: [Foundations, Correctness & Induction]
sources:
  - book: Erickson
    ref: "Ch. 0 — Introduction & Appendix: Induction"
  - book: CLRS
    ref: "Ch. 2 — Loop Invariants; App. — Summations"
  - book: Skiena
    ref: "§1.3 — Reasoning about Correctness"
practice:
  - title: 'Power of Two'
    slug: power-of-two
    difficulty: Easy
  - title: 'Climbing Stairs'
    slug: climbing-stairs
    difficulty: Easy
  - title: 'Sqrt(x)'
    slug: sqrtx
    difficulty: Easy
  - title: 'Happy Number'
    slug: happy-number
    difficulty: Easy
---

Every algorithm in this course comes with [four
deliverables](/algorithms/foundations/what-is-an-algorithm), and the third —
**proof of correctness** — is the one students skip and regret. An algorithm you
cannot argue for is a _conjecture_: it might be right, but you have no way to know,
and "it passed my tests" is not a proof, since one untested instance can sink it.

The arguments you need are few. A small kit of techniques
proves nearly everything in algorithms, and the same shapes recur from sorting to
intractability. This lesson is that kit. None of it is deep; the skill is
recognizing _which_ tool fits a given claim, and writing the argument cleanly
enough that a skeptical reader is forced to agree.

> **Note (What a proof must do).** A proof is a chain of statements, each either an
> assumption, a definition, or a consequence of earlier statements by a rule of
> logic, ending at the claim. The standard of success is adversarial: imagine a
> reader who _wants_ to disbelieve you and will exploit any gap. Your job is to
> leave no gap.

## Direct proof

The default. To prove "if $P$ then $Q$," assume $P$ and walk a chain of valid
steps to $Q$. Most everyday claims yield to it.

> **Claim.** If $n$ is odd, then $n^2$ is odd.

> **Proof.** Assume $n$ is odd. By definition $n = 2k + 1$ for some integer $k$.
> Then $n^2 = (2k+1)^2 = 4k^2 + 4k + 1 = 2(2k^2 + 2k) + 1$, which is $2m + 1$ with
> $m = 2k^2 + 2k$ an integer, odd by definition. $\qed$

The whole move is to **unfold the definitions** (odd means $2k+1$), do the algebra,
then **fold the definition back** (an expression of the form $2m+1$ is odd). Many
direct proofs follow this shape: translate the hypothesis into symbols, manipulate,
translate back.

## Proof by contrapositive

The statements "if $P$ then $Q$" and "if not $Q$ then not $P$" are _logically
equivalent_:

$$
(P \Rightarrow Q) \;\equiv\; (\lnot Q \Rightarrow \lnot P).
$$

So when the forward direction is awkward, prove the contrapositive instead — it is
the **same theorem** in an easier form. We used exactly this to prove a search
routine **sound** in the [previous
lesson](/algorithms/foundations/what-is-an-algorithm): rather than reason about the
whole array ("if $k \notin A$ it returns `not found`"), we reasoned about one line
of code ("if it returns `found` then $k \in A$").

> **Claim.** If $n^2$ is even, then $n$ is even.

> **Proof.** Contrapositive: if $n$ is odd then $n^2$ is odd, which restates the
> direct claim above. Since the contrapositive holds, so does the original. $\qed$

Proving $n^2$ even $\Rightarrow n$ even _directly_ is clumsy (you would factor
$n^2$); the contrapositive reduces it to a one-line consequence of work already
done.

In algorithm design, contrapositives are most useful when they turn a claim about
_absence_ into a claim about _presence_. Here is the argument that lets a trial-division
primality test stop at $\sqrt{n}$ instead of scanning all the way to $n - 1$:

> **Claim.** If $n \ge 2$ has no divisor $d$ with $2 \le d \le \sqrt{n}$, then $n$
> is prime.

> **Proof.** Contrapositive: if $n$ is composite, it has a divisor in that range.
> Write $n = ab$ with $2 \le a \le b < n$; such a factorization exists by the
> definition of composite, and we may name the smaller factor $a$. Then
> $a^2 \le ab = n$, so $a \le \sqrt{n}$, and $a$ is the divisor we promised. $\qed$

The forward statement quantifies over every candidate divisor and asserts a
negative, which gives you nothing to compute with. The contrapositive supplies a
concrete object ($a$, the smaller factor) and one inequality. The algorithmic
payoff is real: testing a twelve-digit number now takes about $10^6$ trial
divisions instead of $10^{12}$.

## Proof by contradiction

To prove $P$, assume **$\lnot P$** and derive an impossibility. Since valid
reasoning from a true premise cannot reach a falsehood, the premise $\lnot P$ must
have been false, so $P$ holds. It is the proof of last resort, and often the
shortest.

$$
% caption: Proof by contradiction: assume the claim is false, reason without error, and
%          arrive at something impossible; the only escape is that the assumption was wrong.
\begin{tikzpicture}[>=Stealth, node distance=8mm,
  box/.style={draw, minimum height=8mm, inner sep=2.4mm, font=\small, align=center}]
  \definecolor{acc}{HTML}{2348F2}
  \node[box, fill=orange!18] (a) {assume the claim is false};
  \node[box, below=of a] (b) {valid, error-free steps};
  \node[box, fill=red!14, below=of b] (c) {a contradiction};
  \node[box, fill=acc!15, right=22mm of b] (d) {so the claim is true};
  \draw[->, thick] (a) -- (b);
  \draw[->, thick] (b) -- (c);
  \draw[->, thick, acc] (c.east) .. controls +(1.4,0) and +(0,-1.2) .. (d.south);
\end{tikzpicture}
$$

The classic is the irrationality of $\sqrt{2}$, the proof the Pythagoreans
reputedly found unsettling.

> **Theorem.** $\sqrt{2}$ is irrational.

> **Proof.** Suppose not: $\sqrt{2} = p/q$ for integers $p, q$ in **lowest terms**
> (no common factor). Squaring, $2q^2 = p^2$, so $p^2$ is even, hence $p$ is even
> (by the contrapositive claim above), say $p = 2r$. Then $2q^2 = 4r^2$, so
> $q^2 = 2r^2$ is even, hence $q$ is even too. But then $p$ and $q$ share the factor
> $2$ — contradicting "lowest terms." The assumption was impossible, so $\sqrt{2}$
> is irrational. $\qed$

Contradiction also proves things _do not exist_ or _cannot be improved_. The
[$\Omega(n\log n)$ lower bound](/algorithms/sorting/sorting-lower-bounds) for
comparison sorting and the proof that [no greedy coin
system](/algorithms/dynamic-programming/coin-change-and-unbounded) is always
optimal are both "suppose a better object existed, derive absurdity" arguments.
Here is the smallest specimen of that genre, a genuine lower bound proved in four
sentences:

> **Theorem.** Any correct algorithm that finds the maximum of $n$ numbers must
> examine all $n$ of them.

> **Proof.** Suppose not: some correct algorithm $\mathcal{A}$, run on some input
> $A$, returns an answer $m$ without ever reading $A[i]$. Build a second input
> $A'$ that agrees with $A$ everywhere except $A'[i] = m + 1$. Since
> $\mathcal{A}$ never reads position $i$, its execution on $A'$ is step-for-step
> identical to its execution on $A$, so it returns $m$ again. But the maximum of
> $A'$ is at least $m + 1 > m$, so $\mathcal{A}$ is wrong on $A'$, contradicting
> its correctness. $\qed$

The move deserves a name, because it recurs: the contradiction is manufactured by
an **adversary** who watches what the algorithm does and then plants the bad case
precisely in the spot it never looked. Every "you cannot do better than $X$"
claim in this course, from [sorting](/algorithms/sorting/sorting-lower-bounds) to
searching, has this shape: assume a faster algorithm exists, then exhibit an
input it must get wrong.

::impl{algo="rational_sqrt"}

## Induction

Induction is the main tool for proving algorithm correctness, because algorithms _repeat_:
loops and recursion both do the same thing on ever-smaller (or ever-larger)
instances.[^erickson-induction] To prove a statement $P(n)$ for **all** $n \ge n_0$,
you show two things:

- **Base case.** $P(n_0)$ holds outright.
- **Inductive step.** _Assuming_ $P(k)$ (the **induction hypothesis**), prove
  $P(k+1)$.

Together these are a falling chain of dominoes: the base case tips the first, the
step guarantees each tips the next, so all of them fall.

$$
% caption: Induction as dominoes: the base case topples the first tile, the inductive step
%          guarantees each tile topples its neighbour, so every tile falls.
\begin{tikzpicture}[>=Stealth]
  \definecolor{acc}{HTML}{2348F2}
  \foreach \k/\x in {1/0, 2/1.0, 3/2.0, 4/3.0, 5/4.0}
    \node[draw, fill=acc!10, minimum width=3.2mm, minimum height=11mm, inner sep=0] (d\k) at (\x,0) {};
  \node[draw, fill=acc!30, draw=acc, very thick, minimum width=3.2mm, minimum height=11mm, inner sep=0] at (0,0) {};
  \foreach \a/\b in {1/2, 2/3, 3/4, 4/5}
    \draw[->, thick] (d\a.north) .. controls +(0.3,0.45) and +(-0.3,0.45) .. (d\b.north);
  \node[font=\footnotesize, acc, align=center, below=1.5mm of d1] {base\\P(1)};
  \node[font=\footnotesize, align=center, below=1.5mm of d4] {step\\P(k) gives P(k+1)};
\end{tikzpicture}
$$

The textbook example is the sum of the first $n$ integers, the same closed form
the [analysis lessons](/algorithms/foundations/asymptotic-analysis) lean on.

> **Claim.** For all $n \ge 1$, $\;1 + 2 + \cdots + n = \dfrac{n(n+1)}{2}$.

> **Proof.** By induction on $n$.
>
> _Base case_ ($n = 1$): the left side is $1$, the right side is $1\cdot 2/2 = 1$. ✓
>
> _Inductive step._ Assume $1 + \cdots + k = \dfrac{k(k+1)}{2}$. Then
>
> $$1 + \cdots + k + (k+1) = \frac{k(k+1)}{2} + (k+1) = \frac{k(k+1) + 2(k+1)}{2} = \frac{(k+1)(k+2)}{2},$$
>
> which is the claim for $k+1$. By induction it holds for every $n \ge 1$. $\qed$

Equalities are the gentlest case, because the inductive step is forced: substitute
the hypothesis, simplify, done. Inequalities require slightly more judgment: after
substituting you must still _bridge_ from what the hypothesis gives you to what
the claim demands. Here is the inequality that explains why halving reaches $1$
in logarithmically many steps, the fact behind [binary
search](/algorithms/foundations/what-is-an-algorithm) and every
divide-and-conquer depth bound:

> **Claim.** For all $n \ge 0$, $\;2^n \ge n + 1$.

> **Proof.** By induction on $n$.
>
> _Base case_ ($n = 0$): $2^0 = 1 \ge 0 + 1$. ✓
>
> _Inductive step._ Assume $2^k \ge k + 1$ for some $k \ge 0$. Then
>
> $$2^{k+1} = 2 \cdot 2^k \ge 2(k+1) = (k + 2) + k \ge k + 2,$$
>
> using the hypothesis for the first inequality and $k \ge 0$ for the second.
> That is the claim for $k + 1$. $\qed$

Read the step closely: the hypothesis delivered $2(k+1)$, the claim wanted
$k + 2$, and the bridge was the observation that the surplus $k$ is nonnegative.
Most failed induction attempts on inequalities die exactly at that bridge, and the
usual repair is to prove a stronger claim whose surplus is bigger.

The art is choosing the hypothesis. Too weak and the step cannot go through; the
fix is often to prove a _stronger_ statement, whose hypothesis gives the step more
to work with (this is **strengthening the induction hypothesis**, and it powers the
[substitution method](/algorithms/foundations/recurrences) for recurrences).

::impl{algo="gauss_sum"}

## Strong induction

Sometimes $P(k+1)$ needs more than its immediate predecessor — it needs _several_
smaller cases, or one you cannot predict in advance. **Strong induction** grants
the entire history: to prove $P(n)$, assume $P(j)$ for **all** $n_0 \le j < n$.

$$
% caption: Ordinary induction leans on the single previous case; strong induction leans on
%          every smaller case at once — needed when a step splits into unpredictable parts.
\begin{tikzpicture}[>=Stealth, every node/.style={font=\small}]
  \definecolor{acc}{HTML}{2348F2}
  \foreach \k/\x in {1/0, 2/1.1, 3/2.2, 4/3.3} {
    \node[draw, circle, minimum size=7mm, inner sep=0, fill=acc!10] (s\k) at (\x,0) {$\k$};
  }
  \node[draw, circle, minimum size=7mm, inner sep=0, fill=acc!25, draw=acc, very thick] (sn) at (4.6,0) {$n$};
  \draw[->, thick] (s1) to[out=55, in=100] (sn.north);
  \draw[->, thick] (s2) to[out=50, in=120] (sn.125);
  \draw[->, thick] (s3) to[out=45, in=140] (sn.150);
  \draw[->, thick] (s4) -- (sn);
  \node[font=\footnotesize, acc, below=4mm of s2] {every smaller case supports $n$};
\end{tikzpicture}
$$

It is the natural argument whenever a problem **splits** into smaller subproblems
of sizes you do not know ahead of time — which is to say, most of [divide &
conquer](/algorithms/divide-and-conquer/mergesort) and [dynamic
programming](/algorithms/dynamic-programming/principles).

> **Claim.** Every integer $n \ge 2$ is a product of primes.

> **Proof.** By strong induction on $n$.
>
> _Base case_ ($n = 2$): $2$ is prime, a product of one prime. ✓
>
> _Inductive step._ Take $n > 2$ and assume the claim for every $j$ with
> $2 \le j < n$. If $n$ is prime, it is its own factorization. Otherwise $n = ab$
> with $2 \le a, b < n$. By the **strong** hypothesis both $a$ and $b$ are products
> of primes, so their product $n$ is too. $\qed$

Ordinary induction would be stuck here: $n$'s factorization has nothing to do with
$(n-1)$'s. Knowing that $12 = 2^2 \cdot 3$ tells you nothing useful about $13$,
and knowing about $13$ tells you nothing about $14 = 2 \cdot 7$. We needed the
freedom to reach back to $a$ and $b$, wherever they landed. For $n = 91$ that
means $a = 7$ and $b = 13$, neither of which is $90$.

::impl{algo="prime_factorization"}

### Strong induction proves recursion correct

The payoff of strong induction is that it certifies recursive algorithms almost
mechanically: assume every recursive call returns the right answer (each call is
on a _smaller_ instance, so the strong hypothesis covers it), then check that the
combining logic is sound.[^erickson-induction] Here is the standard fast
exponentiation routine, which computes $x^n$ in $O(\log n)$ multiplications by
squaring:

```algorithm
caption: $\textsc{Power}(x, n)$ — compute $x^n$ for integer $n \ge 0$
number: 1
if $n = 0$ then
  return $1$
$h \gets \textsc{Power}(x, \lfloor n/2 \rfloor)$ // recurse on the half
if $n$ is even then
  return $h \cdot h$
else
  return $h \cdot h \cdot x$
```

> **Theorem.** For every integer $n \ge 0$, $\textsc{Power}(x, n)$ returns $x^n$.

> **Proof.** By strong induction on $n$.
>
> _Base case_ ($n = 0$): the first line returns $1 = x^0$. ✓
>
> _Inductive step._ Take $n \ge 1$ and assume $\textsc{Power}(x, j) = x^j$ for
> every $j$ with $0 \le j < n$. Since $n \ge 1$ we have
> $\lfloor n/2 \rfloor < n$, so the hypothesis applies to the recursive call and
> $h = x^{\lfloor n/2 \rfloor}$. Two cases:
>
> - $n$ even, say $n = 2m$: then $\lfloor n/2 \rfloor = m$ and the routine
>   returns $h \cdot h = x^m \cdot x^m = x^{2m} = x^n$. ✓
> - $n$ odd, say $n = 2m + 1$: then $\lfloor n/2 \rfloor = m$ and the routine
>   returns $h \cdot h \cdot x = x^m \cdot x^m \cdot x = x^{2m+1} = x^n$. ✓
>
> In both cases the return value is $x^n$, so the claim holds for $n$. $\qed$

Notice which induction was required. The call from input $n$ is on
$\lfloor n/2 \rfloor$, not on $n - 1$: for $n = 100$ the proof for $100$ leans on
the case $50$, skipping the forty-nine cases between. Weak induction's hypothesis
covers only the immediate predecessor and cannot reach that far back. Every
recursive correctness proof in this course follows this template: base case =
the non-recursive branch, hypothesis = "the recursive calls are correct," step =
"the combine logic preserves correctness." The only obligation that varies is
checking the combine.

### Structural induction: trees

Induction is not confined to $1, 2, 3, \dots$: any collection of objects built
from smaller objects of the same kind supports it. Trees are the canonical case:
a binary tree is either a single leaf or a root with two smaller binary trees
hanging off it, so a claim about all binary trees can be proved by inducting on
the tree's size, with the subtrees playing the role of "smaller cases." This is
**structural induction**, and it is strong induction in disguise: a root's
subtrees can be _any_ smaller sizes, so the step needs the full history, exactly
as prime factorization did.

> **Theorem.** Every full binary tree (each internal node has exactly two
> children) with $n$ internal nodes has $n + 1$ leaves.

$$
% caption: A full binary tree with $n = 3$ internal nodes (circles) and $n + 1 = 4$
%          leaves (squares). Removing the root splits it into two smaller full binary
%          trees; the strong hypothesis applies to each.
\begin{tikzpicture}[font=\footnotesize,
  int/.style={circle, thick, minimum size=6.5mm, inner sep=0},
  leaf/.style={minimum size=6mm, inner sep=0}]
  \definecolor{acc}{HTML}{2348F2}
  \node[int, draw=acc, fill=acc!12]        (r)   at (0,0)       {1};
  \node[int, draw=acc, fill=acc!12]        (l)   at (-1.5,-1.2) {2};
  \node[leaf, draw=black, fill=orange!18] (rr)  at (1.5,-1.2)  {a};
  \node[leaf, draw=black, fill=orange!18] (ll)  at (-2.5,-2.4) {b};
  \node[int, draw=acc, fill=acc!12]        (lr)  at (-0.5,-2.4) {3};
  \node[leaf, draw=black, fill=orange!18] (lrl) at (-1.3,-3.6) {c};
  \node[leaf, draw=black, fill=orange!18] (lrr) at (0.3,-3.6)  {d};
  \draw[black, thick] (r) -- (l);
  \draw[black, thick] (r) -- (rr);
  \draw[black, thick] (l) -- (ll);
  \draw[black, thick] (l) -- (lr);
  \draw[black, thick] (lr) -- (lrl);
  \draw[black, thick] (lr) -- (lrr);
  \node[acc, align=left]      at (2.8,-2.6) {3 internal nodes};
  \node[black, align=left] at (2.8,-3.2) {4 leaves};
\end{tikzpicture}
$$

> **Proof.** By strong induction on the number of internal nodes $n$.
>
> _Base case_ ($n = 0$): a full binary tree with no internal node is a single
> leaf: $0$ internal nodes, $1$ leaf, and $0 + 1 = 1$. ✓
>
> _Inductive step._ Take a full binary tree $T$ with $n \ge 1$ internal nodes and
> assume the claim for every full binary tree with fewer. Since $n \ge 1$, the
> root of $T$ is internal, so it has exactly two subtrees $L$ and $R$, each a
> full binary tree. Say $L$ has $n_L$ internal nodes and $R$ has $n_R$. The
> internal nodes of $T$ are the root plus those of the subtrees, so
> $n = n_L + n_R + 1$, and in particular $n_L < n$ and $n_R < n$. By the strong
> hypothesis, $L$ has $n_L + 1$ leaves and $R$ has $n_R + 1$. Every leaf of $T$
> lies in exactly one subtree, so $T$ has
> $(n_L + 1) + (n_R + 1) = (n_L + n_R + 1) + 1 = n + 1$ leaves. $\qed$

The proof never mentions the tree's shape: balanced, degenerate, or lopsided,
the count comes out the same, which is why the figure shows a deliberately skewed
tree. Facts of this kind recur throughout the course: this one bounds the size
of [merge trees](/algorithms/divide-and-conquer/mergesort) and decision trees in
the [sorting lower bound](/algorithms/sorting/sorting-lower-bounds), and its
siblings (a binary tree of height $h$ has at most $2^h$ leaves) are proved by the
same template.[^clrs-trees]

## Where inductions go wrong

Induction fails in stereotyped ways, and each failure mode has a classic
specimen. Knowing them keeps your own proofs honest.

**A valid step cannot rescue a false base.** Consider the claim
"$n^2 \ge 2n + 1$ for all $n \ge 1$." The inductive step is airtight: if
$k^2 \ge 2k + 1$, then

$$
(k+1)^2 = k^2 + 2k + 1 \ge (2k + 1) + (2k + 1) \ge 2(k+1) + 1,
$$

since $2k \ge 1$ for $k \ge 1$. Yet the claim is false: at $n = 1$ we would need
$1 \ge 3$, and at $n = 2$ we would need $4 \ge 5$. The first domino never falls.
The statement only becomes true at $n = 3$ ($9 \ge 7$), so the honest theorem is
"for all $n \ge 3$," with base case $n = 3$. Checking where the base actually
starts is not pedantry: an algorithm proved correct "for all $n \ge 3$" still
needs separate handling for $n = 1$ and $2$, and a recursive implementation hits
those inputs last and crashes on them first.

**Count how far back the step reaches.** A step that uses $P(k)$ and $P(k-1)$
together (the shape of every Fibonacci-flavored claim) needs _two_ base cases,
because the step for $n = 2$ reaches down to $P(0)$, which one base case at
$n = 1$ never established. In general, a step that reaches back $r$ positions
needs $r$ consecutive base cases, and a strong-induction step that recurses to
$\lfloor n/2 \rfloor$ needs the base to cover everything its smallest instances
bottom out on. Erickson's advice is to write the step _first_, see which smaller
cases it consumed, and only then decide what the base must
be.[^erickson-induction]

**Flawed maintenance: all horses are the same color.** The most famous broken
induction "proves" that any $n$ horses are identically colored. _Base case_
($n = 1$): one horse has one color. ✓ _Inductive step:_ given $n + 1$ horses,
remove the first; the remaining $n$ are same-colored by hypothesis. Remove the
last instead; the first $n$ are also same-colored. The two groups **overlap**, so
all $n + 1$ share one color. $\qed$?

$$
% caption: The horses argument needs the two $n$-element groups to overlap. For
%          $n + 1 = 5$ they share horses $2, 3, 4$ — but for $n + 1 = 2$ the groups are
%          $\{1\}$ and $\{2\}$, disjoint, and the step collapses.
\begin{tikzpicture}[font=\footnotesize,
  dot/.style={circle, thick, minimum size=5.5mm, inner sep=0}]
  \definecolor{acc}{HTML}{2348F2}
  \foreach \k/\x in {1/0, 2/1.1, 3/2.2, 4/3.3, 5/4.4}
    \node[dot, draw=black, fill=white] (h\k) at (\x,0) {\k};
  \draw[acc, thick] (1.65,0) ellipse [x radius=2.2, y radius=0.55];
  \draw[orange!85!black, thick] (2.75,0) ellipse [x radius=2.2, y radius=0.78];
  \node[acc] at (0.1,1.0) {f\/irst 4};
  \node[orange!85!black] at (4.4,1.1) {last 4};
  \node[black, align=center] at (2.2,-1.25) {n+1 = 5: the groups\\share horses 2, 3, 4};
  \node[dot, draw=black, fill=white] (g1) at (6.9,0) {1};
  \node[dot, draw=black, fill=white] (g2) at (8.3,0) {2};
  \draw[acc, thick] (6.9,0) circle [radius=0.5];
  \draw[orange!85!black, thick] (8.3,0) circle [radius=0.5];
  \node[acc] at (6.9,1.0) {f\/irst 1};
  \node[orange!85!black] at (8.3,1.1) {last 1};
  \node[black, align=center] at (7.6,-1.25) {n+1 = 2: the groups\\share no horse};
\end{tikzpicture}
$$

The flaw is quantifier-shaped: the overlap argument silently assumes the two
groups share at least one horse, which requires $n + 1 \ge 3$. At the very first
application of the step (from $n = 1$ to $n = 2$) the groups are $\{1\}$ and
$\{2\}$ with empty intersection, and nothing links their colors. One broken link,
at exactly one value of $n$, and every later domino stands: the proof is valid
for "any $n$ horses of which some two share a color," a theorem nobody needs.
The lesson is to test the inductive step _at its smallest instance_, where
degenerate geometry (empty overlaps, single elements, zero-length ranges) lives.

**Assuming what you are proving.** The inductive hypothesis is $P(k)$; the
obligation is $P(k+1)$. Writing "assume $P(k+1)$" and simplifying it into a true
statement proves nothing, because false premises can yield true conclusions:
from $1 = 2$, multiplying both sides by $0$ gives the perfectly true $0 = 0$.
This mistake usually appears disguised as "start with the
equation for $k+1$ and manipulate both sides until they match." The repair is
directional discipline: start from the _left side_ of the $k+1$ claim (or from
the hypothesis), and transform it by known-valid steps until the right side
appears, never touching the target equation as if it were already true.

## Proof by construction

To prove something **exists**, the most convincing move is to _build it_ — exhibit
the object and check it works. A constructive existence proof produces a witness,
not merely a guarantee.

> **Claim.** There are arbitrarily long runs of consecutive composite numbers — gaps
> between primes can be as wide as you like.

> **Proof.** Given any length $k$, the $k$ consecutive integers
> $$(k+1)! + 2,\;\; (k+1)! + 3,\;\; \dots,\;\; (k+1)! + (k+1)$$
> are all composite: the $i$-th of them, $(k+1)! + i$ for $2 \le i \le k+1$, is
> divisible by $i$ (since $i$ divides $(k+1)!$ and divides $i$). That is an explicit
> run of $k$ composites. $\qed$

This is the proof style closest to our subject, because **an algorithm _is_ a
constructive proof**: a correct algorithm for a problem is a witness that a
solution exists _and_ a recipe for producing it. When the [greedy
method](/algorithms/greedy/the-greedy-method) proves its choice is safe by an
**exchange argument** — take any optimal solution, transform it into the greedy one
without making it worse — that, too, is construction: it builds the optimum it
claims exists.

::impl{algo="prime_gap_construction"}

## Disproof by counterexample

The arguments above _confirm_ universal claims ("for all $n$…"). To **refute** one,
you need just a single instance where it fails. One counterexample is fatal; no
amount of confirming examples can rescue a false "for all."

> **Claim (false).** The greedy rule "always take the largest coin that fits" makes
> optimal change in every currency.

> **Disproof.** Take coin denominations $\{1, 3, 4\}$ and a target of $6$. Greedy
> picks $4$, then $1 + 1$, for three coins. But $3 + 3$ makes $6$ in **two**. One
> instance is enough: the claim is false. $\qed$

This is why correctness must hold on _every_ input, and why a plausible heuristic
needs a proof rather than a few passing trials. Hunting for a small counterexample
is also the fastest way to test a conjecture before investing in a
proof[^skiena-correctness] — a conjecture that survives honest attempts to break
it is worth the cost of a proof.

::impl{algo="greedy_coin_counterexample"}

## Loop invariants are induction

The reason induction matters so much here is that **loop invariants are induction
applied to time**. A loop invariant is a statement true _before and after every
iteration_; proving it amounts to an induction over the iteration count, and its
three-part rubric[^clrs-invariant] maps one-to-one onto the parts of an inductive
proof:

| Loop invariant | Induction |
| --- | --- |
| **Initialization** — holds before the first iteration | **Base case** |
| **Maintenance** — if it holds before a pass, it holds after | **Inductive step** |
| **Termination** — what the invariant gives once the loop stops | **Conclusion** $P(n)$ |

We proved [`Find-Max`](/algorithms/foundations/what-is-an-algorithm) correct exactly
this way, and the pattern returns for every loop in the course. To see the rubric
run end-to-end once more, here is the simplest loop that computes anything:

```algorithm
caption: $\textsc{Array-Sum}(A)$ — return $A[1] + A[2] + \cdots + A[n]$
number: 2
$s \gets 0$
for $i \gets 1$ to $n$ do
  $s \gets s + A[i]$ // fold in the element under the cursor
return $s$
```

> **Invariant.** At the start of the iteration with cursor $i$, the accumulator
> satisfies $s = A[1] + A[2] + \cdots + A[i-1]$: the sum of exactly the elements
> the loop has already visited.

$$
% caption: The invariant photographed mid-run on $A = \langle 4, 1, 6, 2, 7, 3\rangle$ at
%          the start of the iteration with $i = 5$: the accumulator $s = 13$ equals the sum
%          of the shaded prefix $A[1..4]$, and positions $5..6$ are still untouched.
\begin{tikzpicture}[font=\footnotesize]
  \definecolor{acc}{HTML}{2348F2}
  \foreach \x in {0, 0.9, 1.8, 2.7}
    \fill[acc!12] (\x,0) rectangle (\x+0.9,0.72);
  \foreach \x/\v in {0/4, 0.9/1, 1.8/6, 2.7/2, 3.6/7, 4.5/3} {
    \draw[black] (\x,0) rectangle (\x+0.9,0.72);
    \node at (\x+0.45,0.36) {\v};
  }
  \foreach \k/\x in {1/0, 2/0.9, 3/1.8, 4/2.7, 5/3.6, 6/4.5}
    \node[font=\scriptsize, black] at (\x+0.45,-0.24) {\k};
  \draw[acc, very thick] (3.6,0) rectangle (4.5,0.72);
  \draw[acc, thick] (0,-0.55) -- (3.6,-0.55);
  \draw[acc, thick] (0,-0.55) -- (0,-0.44);
  \draw[acc, thick] (3.6,-0.55) -- (3.6,-0.44);
  \node[acc, align=center] at (1.8,-1.05) {already summed\\s = 4+1+6+2 = 13};
  \draw[->, thick, acc] (4.05,1.55) -- (4.05,0.88);
  \node[acc] at (4.05,1.85) {cursor i = 5};
  \node[black, align=center] at (6.15,0.36) {not yet\\seen};
\end{tikzpicture}
$$

- **Initialization.** Before the first iteration, $i = 1$ and the invariant reads
  $s = $ (sum of no elements) $ = 0$. The seed line set $s \gets 0$, and the
  empty sum is $0$ by convention. ✓
- **Maintenance.** Assume the invariant entering the iteration with cursor $i$:
  $s = A[1] + \cdots + A[i-1]$. The body executes $s \gets s + A[i]$, after which
  $s = A[1] + \cdots + A[i-1] + A[i]$ — the invariant with cursor value $i + 1$,
  the state in which the next iteration begins. ✓
- **Termination.** The loop exits when the cursor passes $n$, i.e. with the
  invariant holding for $i = n + 1$: $s = A[1] + \cdots + A[n]$. That is the
  specified output, and the last line returns it. ✓

Each bullet is short because the invariant was chosen well: it names the one
quantity the loop maintains, at one fixed instant (the _start_ of an iteration),
and it mentions the cursor so that termination instantiates it at a known value.
A vaguer statement ("$s$ holds a partial sum") passes initialization and
maintenance trivially and then gives you nothing at termination. The rubric only
pays off if the invariant is strong enough that its $i = n + 1$ instance _is_ the
correctness claim.[^clrs-invariant]

Recursion is even more direct: a recursive algorithm is correct by (usually
strong) induction on the size of its input, with the base case the non-recursive
branch and the inductive step the assumption that the recursive calls are
themselves correct, exactly the $\textsc{Power}$ proof above.

::impl{algo="find_max_invariant"}

## A note on yes/no algorithms

For procedures that **decide** rather than compute — does a path exist, is this
formula satisfiable, is $k$ in the array — correctness has two halves with standard
names, introduced [earlier](/algorithms/foundations/what-is-an-algorithm):
**soundness** (every _yes_ is true — no false positives) and **completeness** (every
true case is caught — no false negatives). The two are proved separately and often
with different tools: soundness frequently falls to a direct or contrapositive
argument about a single accepting step, while completeness usually wants induction
over the algorithm's progress. Keeping them apart keeps the proof honest.

## Machine-checked proof, and its limits

Every technique here is a _paper-and-pencil_ proof, checked by a human reader.
Two developments push past that. The first is **machine-checked proof**: an
a proof assistant like Coq, Lean, or Isabelle can check an inductive argument
mechanically, invariant by invariant, with no gap left to
"clearly." The four-color theorem (1976) was the first famous result whose proof
had to be completed by computer, and modern formalizations — Gonthier's fully
machine-checked four-color and Feit–Thompson proofs — show the same induction and
case analysis we do by hand, scaled to sizes no referee could audit.[^formal-proofs]
When a correctness proof matters enough that a subtle error would be costly, this
is where the discipline of "state the invariant precisely" pays off.

The second is a caution about **what a proof of correctness does and does not
buy**. A verified algorithm is correct _relative to its specification_; if the
specification is wrong, the proof certifies the wrong thing. And correctness is
separate from feasibility: proving that a procedure eventually halts with the
right answer says nothing about whether it halts before the sun burns out — the
running-time analysis of the [next lessons](/algorithms/foundations/asymptotic-analysis)
is a distinct obligation. Skiena's running advice, to attack a conjecture with
small counterexamples _before_ attempting a proof, is the cheap filter that
saves the expensive one: most false conjectures die to an instance with three or
four elements.[^skiena-counterexamples]

## Takeaways

- **Match the tool to the claim.** "If $P$ then $Q$" → direct, or contrapositive if
  the reverse is easier. A "for all $n$" about a repeated process → induction (strong
  induction when a step needs many smaller cases). "There exists" → construction.
  "This always works" that you doubt → hunt a counterexample.
- **Induction is the spine of correctness proofs**, because loops and recursion
  repeat. Loop invariants are induction over iterations; recursive correctness is
  induction over input size.
- **Strengthen the hypothesis** when an inductive step won't close — proving a
  stronger statement can be _easier_, because the step gets more to work with.
- **Audit the base and the smallest step.** A valid inductive step cannot rescue
  a false base case, a step that reaches back $r$ positions needs $r$ base cases,
  and flawed maintenance hides at the smallest instance (the horses "proof"
  breaks only at $n + 1 = 2$).
- **One counterexample refutes a universal claim**; no finite pile of examples
  proves one. This is why "it passed the tests" is evidence, not proof.
- **An algorithm is a constructive existence proof** — which is why getting the proof
  right and getting the algorithm right are the same task, not two.

[^erickson-induction]: **Erickson**, _Algorithms_, Appendix on Induction — the "boilerplate" inductive proof and the discipline of an explicit, strong induction hypothesis.
[^clrs-invariant]: **CLRS**, Ch. 2 (§2.1) — loop invariants and the initialization / maintenance / termination rubric.
[^skiena-correctness]: **Skiena**, _The Algorithm Design Manual_, §1.3 — reasoning about correctness, and counterexamples as the first line of attack on a conjecture.
[^clrs-trees]: **CLRS**, Appendix B.5 — trees and their basic counting properties; the decision-tree argument that uses them appears in Ch. 8 (§8.1).
[^formal-proofs]: Appel, K. & Haken, W. (1977). "Every planar map is four colorable." _Illinois J. Mathematics_ 21 — the first computer-assisted proof; Gonthier, G. (2008). "Formal proof — the four-color theorem." _Notices of the AMS_ 55(11), and the machine-checked Feit–Thompson odd-order theorem (2012).
[^skiena-counterexamples]: **Skiena**, _The Algorithm Design Manual_, §1.3 — hunting small counterexamples as the first, cheapest test of a conjectured algorithm or claim.