The five proof errors

Consider a collection consisting of a single horse, which is evidently the same colour as itself — monochromatic, one colour throughout — so the initial case of an induction is satisfied. For the inductive step, take n+1 horses and examine the first n together with the last n. Each block is a collection of n horses and is monochromatic by assumption. The blocks overlap in n−1 horses, so all n+1 horses share a single colour [S:5:132].

The base case is correct, the step appears impeccable, and the conclusion is demonstrably false [S:5:132]. It is the model for the five mistakes in this section, each of which resembles a proof until the joint where it fails is located. !The step carries the colour across the overlap, and at the rung the proof needs, the overlap is empty. Each row lists $n+1$ horses, with the first $n$ bracketed above and the last $n$ below; the tint is the horses in both brackets. With four horses and with three, the tint holds two horses and then one, and the colour passes. With two horses the list is $h_1,h_2$, the upper bracket holds $h_1$ alone and the lower holds $h_2$ alone, so the tint is an empty outline and nothing carries a colour from one block to the other. Status: schematic.

Worked example. Identify the sentence that fails, and determine the value of n at which the failure occurs.

Formulate the step at the smallest index where it could fail, and replace every ellipsis — each "and so on" standing in for the middle of a list — by an actual object. At n = 1 the list is h₁, h₂. The initial block consists of h₁ alone, and the final block consists of h₂ alone. The two blocks have no horse in common, so nothing transmits a colour from one to the other [S:5:132].

The failure is not the base case, which is correct, and it is not the selection of index one, which is entirely legitimate. The failure is that the overlap, which performs the entire work, is empty at exactly the rung where the step has to work.

The five shapes follow below in reading order, and the horse argument above is the third of them. Each has a name and a question that detects it, and the names are worth knowing cold, because a reader who knows them can inspect a proof one joint at a time. The alternative is to read the argument and wait for something to feel wrong, and that feeling is not a reliable instrument. A proof is a finite object with a limited number of joints, and nearly every failure occurs at a joint: a direction, an index, a constant, a hypothesis.

The first error is proving the converse, the sentence you get by swapping hypothesis and conclusion. A benchmark is a fixed test set with recorded scores, and take the claim "if the method works, the benchmark improves". From it together with "the benchmark improved" nothing follows about the method, because a benchmark can improve for a multitude of unrelated reasons. The valid neighbour is contraposition: from "if the benchmark does not improve, the method does not work" you may infer the original claim [S:5:18]. The difference is a single reversed arrow, and the error is the most frequent one in reading a table of results.

The second error is a proof that runs backwards. Commence from the claim that the arithmetic mean of two numbers is at least their geometric mean, where the arithmetic mean is half their sum and the geometric mean is the square root of their product. Rearrange until you reach (a − b)² ≥ 0, and observe that the final line is correct.

The final line is correct, and the argument has assumed the very proposition that it was asked to establish [S:5:30]. A true sentence that follows from a claim is no evidence for the claim, because false claims imply true sentences too. The repair is a reordering of the lines, which is why the error is easy to commit and easy to overlook.

The third error is an unchecked index, a step checked in general but never at the smallest index. The horse argument is the example: its step is true for every n from two upwards, and at n = 1 the ellipsis concealed an empty overlap, so the chain never starts. The general statement is checked, the smallest case is not, and the argument reads as complete because the general statement is the one you see [S:5:132].

The fourth error is a constant that is not constant. The claim that 2ⁿ is bounded by a constant says that one fixed number c satisfies 2ⁿ ≤ c for every n. A proof of it proceeds as follows: assume 2ⁿ ≤ c, then 2ⁿ⁺¹ = 2 × 2ⁿ ≤ 2c, so the bound holds with a new constant 2c [S:5:554]. The constant altered during the argument, which means that there was never a single constant to begin with. The claim is false, and the proof is a quantifier error expressed in ordinary English with no symbol anywhere in sight.

The fifth error is an unchecked hypothesis, a condition that must hold before a rule applies. From 1 = √1 = √((−1)(−1)) = √(−1) × √(−1) = −1, the rule that a square root of a product equals the product of the square roots has been applied where it does not hold [S:5:29]. The rule holds for non-negative factors, and the line applies it to two negative ones; it also treats √(−1), which is not a real number, as one. Every line is correct except the one where the rule was applied, which explains why the error survives a cursory inspection.

The list is not exhaustive, and it cannot be. It catalogues the modes in which proofs have failed often enough to be named, and an unprecedented kind of error is unprecedented. That is why the fifth error is the hardest to teach: it asks about the hypothesis of a rule, which takes a habit of checking rather than a memory for shapes. Even a plausible argument can be wrong in a way no catalogue predicted.

Fermat's last theorem, which says that no whole number solution of xⁿ + yⁿ = zⁿ exists for n greater than 2, was proved by Wiles, whose first proof was wrong and whose corrected version appeared a year later [S:5:15]. The five interrogations raise the chance of detection and do not remove the chance of failure.

The formal statement. Each error is a failure of one inference. To check a proof, locate the rule that licenses each line and check its premises. The five shapes become five different faults. Each shape is then a sentence about the scope of a word.

The converse. From the conclusion of an implication and the implication itself, nothing follows about the hypothesis. Set the hypothesis false and the conclusion true, and both premises hold. The sound neighbour: from a false conclusion and a true implication, infer a false hypothesis [S:5:18]. The core's benchmark example is that row: the benchmark can improve for unrelated reasons.

The reversed direction. A chain of implications runs from established sentences to new ones. If every step is reversible, the chain may be read backwards. If one step is not reversible, the chain may not be. The mean-inequality proof that starts at the claim and ends at a square is repairable because its steps are reversible [S:5:30]. A chain that squares cannot be reversed at all.

The missing rung. The horse argument proves the case at one, and it proves the step for every $n$ from two upwards. Induction needs the step at one. At that index the blocks are one horse each, with empty overlap [S:5:132]. The argument therefore gives the base case and a step that begins one rung too high, and the chain below that rung never moves.

The moving constant. The claim is that some constant $c$ bounds every $2^n$. The step proves that a bound at $n$ yields twice that bound at $n+1$. Read as a proof of the claim, it fixes nothing: the constant is chosen after $n$, so the argument establishes that every $n$ has some bound. That sentence is true and weaker than the claim, and no symbol in the bogus proof marks the difference [S:5:554].

The unchecked hypothesis. The square-root-of-a-product rule holds for non-negative factors, and the bogus line applies it to two negative factors [S:5:29]. The logarithm case is the same fault: the logarithm of one half is negative, so multiplying by it reverses the inequality. A rule is a conditional, and its hypothesis is part of the rule.

The edge case. A valid proof from a false hypothesis establishes nothing about the world. "If one equals two then one equals one" is true and useless. Validity preserves truth; it does not create it. The mean inequality argument has a true conclusion and a broken proof, so a correct answer is not evidence for the argument that produced it.

Where the joints analogy breaks. A proof has joints, and most faults sit at one. Some do not: a wrong definition damages every line at once, and no local check finds it. The five shapes are symptoms with named causes, not a partition: the horse error is at once a missing rung and an unchecked hypothesis about the overlap.

What the core left out. It left out the rule that licenses each step, because the core reads proofs in English. In a formal system the licence is explicit, and the machine rejects a line with no rule [S:5:18]. That is why the five errors become compile errors, and why the informal argument remains where they are made.

Original sources. The five shapes are drawn from the bogus-proof problems of Mathematics for Computer Science, where each is stated as a claim with a proof to be repaired [S:5:29]. The horse induction is section 5.1, and the diagnosis names the ellipsis as the place where the overlap disappears [S:5:132]. The historical cases are in section 1.1: the four-colour proof that stood for ten years, and Wiles' first proof [S:5:15].

An open question. The catalogue is finite and the space of faults is not. Whether a finite list can be complete is open in the only sense that matters: a new fault appears when someone invents an argument that no row describes. Evidence that would settle it: a large corpus of proofs with machine-checked kernels, human-classified errors, and a classification that stays stable as the corpus grows. If new classes keep appearing at a steady rate, the catalogue is a checklist and not a theory.

A frontier result. Kernel checking moves detection from the reader to the machine. A proof assistant accepts a proof only when every step is licensed, so the five faults become failures to compile rather than failures of judgement [S:603:2]. Neural provers are trained against that signal, and the current numbers on competition mathematics are high on one benchmark and low on another: 88.9% on MiniF2F and 47 of 658 on PutnamBench [S:604:1]. The five errors survive in the informal argument that precedes the formal one, and the formalisations in the benchmark are still written by hand [S:603:2].

What to read next. Read the problem sets of [S:5:29] for the bogus proofs and section 5.1 of [S:5:132] for the induction that fails. Read the background section of [S:603:2] for what a kernel guarantees, and [S:604:1] for the prover trained against it. Then read section 1.1 of [S:5:15] for the two historical failures, because a checked proof of the wrong statement is still wrong.