What Is Proof by Cases? Checking Every Possibility When There Are Not Too Many

The approach establishes a general claim by showing that the possibilities fall into a finite number of cases and that the claim holds in each. The essential requirement is exhaustiveness, meaning the cases genuinely cover everything, since a proof that checks most possibilities establishes nothing, and constructing a provably complete case division is frequently the hard part rather than the checking. The cases need not be equally sized or similar, and a proof may handle one case in a line and another over several pages. Where the number of cases is small the method is unremarkable and appears throughout mathematics, generally without being named. Where the number is large it becomes a different kind of object, and where it exceeds what a person can verify it becomes contentious.

The method appears constantly in ordinary mathematics without attracting attention:

• •Proving a statement about whole numbers by treating even and odd separately
• •Proving a result about absolute values by considering positive, negative and zero
• •Establishing a geometric claim by checking each possible configuration of the figure
• •Proving that a given property holds for every remainder when divided by a fixed number, which reduces an infinite claim to finitely many cases
• •Checking a small finite structure completely, such as verifying a claim about all graphs with at most a certain number of vertices
• •Establishing a base case for an induction, which is the same move at smaller scale

The most famous instance concerns whether four colours suffice to colour any map so that adjacent regions differ, which was conjectured in 1852 and resisted proof for over a century. The proof announced in 1976 reduced the problem to a finite set of configurations, over a thousand of them, and verified each by computer, which was the first major theorem established that way. The reaction was substantial and divided. Some mathematicians accepted it as a proof. Others objected that a proof should be surveyable by a human, that nobody could check the computation by hand and that confidence therefore rested on trusting hardware and software rather than on mathematical understanding. Subsequent work reduced the number of configurations, produced independent implementations and eventually generated a version verified by a proof-checking program, which addresses the software concern by a different route.

The method only applies where the possibilities are genuinely finite, and a great deal of mathematics concerns claims about infinitely many objects where no list exists. That is why other methods dominate, including induction, which handles infinitely many cases by relating each to the next, and direct argument from definitions, which establishes a claim for an arbitrary object and therefore for all of them. Reducing an infinite problem to a finite one is itself a substantial achievement when it can be done, and the four colour proof consists mostly of that reduction rather than of the checking. Comparable reductions underlie several other computer-assisted results, including work on sphere packing. The pattern in each is that human mathematics does the reduction and computation does the enumeration, which is a division of labour rather than a replacement.

The dispute raised a question that has not gone away as computation has become more central. One view holds that a proof is whatever establishes truth reliably, so a computation checked by independent implementations is at least as trustworthy as a long human argument, given that human proofs contain errors and that several published results have been wrong for years. Another holds that a proof should explain why something is true and that an exhaustive check explains nothing, delivering certainty without understanding, which is a claim about what mathematics is for rather than about reliability. Formal verification systems, which check a proof step by step against the axioms, have been applied to major theorems and offer a third position, since they deliver machine-checkable certainty and are themselves unreadable. The practice has moved on and the disagreement about what it means has not been settled.

Dividing the possibilities into a finite list and checking each is rigorous provided the list genuinely covers everything, which is usually the hard part. The four colour theorem was proved this way in 1976 with over a thousand computer-checked configurations, which divided mathematicians over whether a proof nobody can survey by hand is a proof.