Somewhere on this site, an exercise told you that testing is not proof. It showed you a “for all” over infinitely many values, ran a few hundred samples, found no counterexample, and then said it plainly: that is not the same as proving it. This article explains what does prove it. The technique is called mathematical induction. You already use its structure whenever you write a recursive function.
The claim that covers everything
These sentences sound similar. They do not mean the same thing:
- “It works for the inputs I tried.”
- “It works for every input.”
Testing gives you the first. A proof gives you the second. Induction proves claims over the natural numbers - 0, 1, 2, 3, and on forever - without running all of them.
The claim has a useful shape. You want to prove that a property P holds for every natural number. You cannot check them one by one, but you can prove two smaller things:
- The base case: P holds for 0.
- The inductive step: if P holds for some number k, then P holds for k + 1.
If both are true, the claim is proven. P(0) holds, so the step gives you P(1); apply it again and you get P(2), then P(3), and so on. The base case starts the chain. The step provides every next link. Two finite arguments prove infinitely many facts.
This is not a hand-wave. The step is a general argument: for any k, if P(k) holds, then P(k + 1) holds. It concerns the shape of the step, not a specific number, so it covers every step at once. That is the whole trick: a universal claim can be proven by a base case plus a general step.
The skeleton
Every induction proof has the same four lines. This one proves that n < 2^n for every natural number n:
- Claim: n < 2^n for every natural n.
- Base case: 0 < 2^0 = 1, true.
- Inductive hypothesis: assume k < 2^k for some natural k.
- Inductive step: since k and 2^k are integers, k < 2^k means k + 1 <= 2^k. And 2^k <= 2^k + 2^k = 2^(k+1). So k + 1 < 2^(k+1), which is exactly the claim for k + 1.
Conclusion: by induction, n < 2^n for every natural n.
The proof never picks a large n and checks it. That would not help: a billion checks still leave n + 1 unchecked. The proof works because its step is a general argument that carries the claim from any k to k + 1.
The inductive hypothesis IS the recursive call
Here is the connection this site is built around. Compare the proof above with a recursive function:
def sum([]), do: 0
def sum([head | tail]), do: head + sum(tail)A recursive function has a base clause and a recursive clause. An induction proof has a base case and an inductive step. The correspondence is not accidental. It is the same shape wearing two hats:
| The proof | The function |
|---|---|
| Base case: the claim holds for the smallest input | Base clause: the function returns without recursing |
| Inductive hypothesis: assume the claim for a smaller input | The recursive call: trust the function on a smaller input |
| Inductive step: use the hypothesis to prove the next case | The recursive clause: combine the recursive call’s result |
The middle line surprises people. In the proof, the line “assume sum(t) is correct for the tail t” does the same job as the recursive call sum(tail): it trusts the smaller case. When you write head + sum(tail), you assume the function already works on the tail, just as the proof assumes the claim for the smaller input. The site’s bridge exercises use this connection: they put a proof and a function side by side and ask you to find the line of the proof that is the recursive call.
Writing a correct recursive function and writing an induction proof use the same skill. Every recursive function you trust is an induction proof you did not write down. The base clause is the base case. The recursive call on a smaller input is the hypothesis. The clause body is the step. When the grader checks your sum/1 against test cases, it checks the base and a few steps; the reason the function works for every list is the induction.
Structural induction: lists instead of numbers
Induction is not limited to numbers. It works on structures with a notion of “smaller”: lists, trees, expressions. For lists, “smaller” means “the tail”. The proof that sum adds up every list looks like this:
- Claim: for every list xs of naturals, sum(xs) adds up exactly the elements of xs.
- Base case: sum([]) = 0, the sum of no elements.
- Inductive hypothesis: assume sum(t) is correct for the tail t.
- Inductive step: sum([h | t]) = h + sum(t), which is correct by the hypothesis.
- Conclusion: by structural induction, sum is correct for every list.
The recursion exercises on this site - sum/1, list_length/1, member/2,
reverse/1 - are structural inductions over lists, written as code. If you can write them, you can do this proof. The exercises make you write the code first.
Termination is the same shape
Induction proves more than “the answer is right”. It also proves “the function finishes”. Consider:
def factorial(0), do: 1
def factorial(n) when n > 0, do: n * factorial(n - 1)Why does factorial terminate for every natural n? Induction gives the answer:
- Base: factorial(0) terminates immediately.
- Step: if factorial(k) terminates, then factorial(k + 1) evaluates k + 1 and calls factorial(k), which terminates by the hypothesis - so factorial(k + 1) terminates.
The line “if factorial(k) terminates” does the same job as the recursive call factorial(n - 1): both trust the smaller case. A function that recurses on a smaller input and a proof that steps from k to k + 1 are the same machine viewed from two sides.
Why this is not circular
The natural objection is: “you assumed the claim for k to prove it for k + 1 - isn’t that what you’re trying to prove?” No. The hypothesis is used only at a strictly smaller argument - k, the tail t, or n - 1 - and the chain bottoms out at the base case. You never assume the claim at the size you are proving; you assume it one step down. The base case anchors the argument and keeps it from becoming a loop of assumptions, just as the base clause keeps a recursive function from recursing forever.
What induction is not
- Not a loop. A proof has no runtime. The step is a static argument that covers every k at once; nothing is executed.
- Not “it worked for the first few”. Five true cases prove nothing. The proof is the general step, not the samples.
- Not a blank check. Induction cannot prove a false claim. If the step fails, the proof fails - try “n = n + 1” and the step collapses. The structure guarantees the argument is valid, not that the claim is true.
- Not a substitute for the base case. A correct step with no base proves nothing. Both halves are load-bearing.
The site’s ladder
The quantifier exercises draw the line you met at the top: over a finite domain, enumeration decides; over an infinite domain, the oracle only samples, and the banner says testing is not proof. The lambda exercises make the same point - their bridge for an infinite claim reads: “You CAN’T loop all integers. That’s why you need induction.”
Induction resolves both. It converts a “for all” over an infinite domain from a hope into a guarantee with a base case and a general step.
The induction exercises practice it three ways. The recursion exercises make you write the proof as code - base clause and recursive clause, graded by execution. The bridge exercises make the correspondence explicit: they show a proof and a function side by side and ask which clause is the base case, which line is the inductive hypothesis, and in what order the steps go. The Lean exercises go all the way: the proof is checked by the Lean kernel, a checker that accepts nothing on faith - the same discipline as this site’s oracles, where correctness is decided by verification and never by assertion.
Why this matters here
Induction is where the threads of this site meet. The trace exercises teach you to predict what code does, step by step - that is direct reasoning, the raw material of a proof. The quantifier exercises teach you the difference between testing and proving. The lambda exercises teach you that self-application, run, is recursion - their fixed-point exercises are inductions you can execute. The induction exercises name the connection: a recursive function and an inductive proof have the same shape, and the reason you can trust either is the same reason.
The proofs article said it first: induction is the proof technique that says “every natural number”, and it has the same shape as the recursion you write. This article unpacks that claim. When you write a recursive function and it works for every input, you are not hoping - you are proving.
Where to go next
-
Recursion: the pattern that calls itself
- the code half of the pair: the base case and the step, written as functions instead of claims.
- How to read a proof exercise - the mechanics of a proof, for when the claim to be proved is not about natural numbers but about whatever the exercise is showing.
-
Dynamic programming: recursion with a cache
- induction wearing asymptotic notation: the recursion tree’s levels, and the proof that the recursion covers every case.
- Sorting: the wall at n log n - the recursion-tree analysis is an induction argument; the wall is the theorem the induction proves.