Proof by exhaustion, also known as proof by cases, perfect induction, or the brute force method, is a method of mathematical proof

Mathematical proof

In mathematics, a proof is a convincing demonstration that some mathematical statement is necessarily true. Proofs are obtained from deductive reasoning, rather than from inductive or empirical arguments. That is, a proof must demonstrate that a statement is true in all cases, without a single...

 in which the statement to be proved is split into a finite number of cases and each case is checked to see if the proposition in question holds. A proof by exhaustion contains two stages:

1. A proof that the cases are exhaustive; i.e., that each instance of the statement to be proved matches the conditions of (at least) one of the cases.
2. A proof of each of the cases.

In the Curry–Howard isomorphism, proof by exhaustion and case analysis

Case analysis

Case analysis is one of the most general and applicable methods of analytical thinking, depending only on the division of a problem, decision or situation into a sufficient number of separate cases. Analysing each such case individually may be enough to resolve the initial question...

 are related to ML-style pattern matching

Pattern matching

In computer science, pattern matching is the act of checking some sequence of tokens for the presence of the constituents of some pattern. In contrast to pattern recognition, the match usually has to be exact. The patterns generally have the form of either sequences or tree structures...

.

Example

To prove that every integer

Integer

The integers are formed by the natural numbers together with the negatives of the non-zero natural numbers .They are known as Positive and Negative Integers respectively...

 that is a perfect cube

Cube (arithmetic)

In arithmetic and algebra, the cube of a number n is its third power — the result of the number multiplying by itself three times:...

 is either a multiple of 9, or 1 more, or 1 less than a multiple of 9.

Proof:

Each cube number is the cube of some integer n. This integer n is either a multiple of 3, or 1 more or 1 less than a multiple of 3. So these 3 cases are exhaustive:

• Case 1: If n = 3p, then n³ = 27p³, which is a multiple of 9.
• Case 2: If n = 3p + 1, then n³ = 27p³ + 27p² + 9p + 1, which is 1 more than a multiple of 9. For instance, if n = 4 then n³ = 64 = 9x7 + 1.
• Case 3: If n = 3p − 1, then n³ = 27p³ − 27p² + 9p − 1, which is 1 less than a multiple of 9. For instance, if n = 5 then n³ = 125 = 9×14 − 1.

How many cases?

There is no upper limit to the number of cases allowed in a proof by exhaustion. Sometimes there are only two or three cases. Sometimes there may be thousands or even millions. For example, rigorously solving an endgame puzzle

Chess problem

A chess problem, also called a chess composition, is a puzzle set by somebody using chess pieces on a chess board, that presents the solver with a particular task to be achieved. For instance, a position might be given with the instruction that White is to move first, and checkmate Black in two...

 in chess

Chess

Chess is a two-player board game played on a chessboard, a square-checkered board with 64 squares arranged in an eight-by-eight grid. It is one of the world's most popular games, played by millions of people worldwide at home, in clubs, online, by correspondence, and in tournaments.Each player...

 might involve considering a very large number of possible positions in the game tree

Game tree

In game theory, a game tree is a directed graph whose nodes are positions in a game and whose edges are moves. The complete game tree for a game is the game tree starting at the initial position and containing all possible moves from each position; the complete tree is the same tree as that...

 of that problem.

The first proof of the four colour theorem was a proof by exhaustion with 1,936 cases. This proof was controversial because the majority of the cases were checked by a computer program, not by hand. The shortest known proof of the four colour theorem today still has over 600 cases.

Mathematicians prefer to avoid proofs with large numbers of cases. Such proofs feel inelegant to them. A proof with a large number of cases leaves an impression that the theorem is only true by coincidence, and not because of some underlying principle or connection. Other types of proofs—such as proof by induction (mathematical induction

Mathematical induction

Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...

)—are considered more elegant. However, there are some important theorems for which no other method of proof has been found, such as

• The proof that there is no finite projective plane
  Projective plane
  In mathematics, a projective plane is a geometric structure that extends the concept of a plane. In the ordinary Euclidean plane, two lines typically intersect in a single point, but there are some pairs of lines that do not intersect...
  
   of order 10.
• The classification of finite simple groups
  Classification of finite simple groups
  In mathematics, the classification of the finite simple groups is a theorem stating that every finite simple group belongs to one of four categories described below. These groups can be seen as the basic building blocks of all finite groups, in much the same way as the prime numbers are the basic...
  
  .
• The Kepler conjecture
  Kepler conjecture
  The Kepler conjecture, named after the 17th-century German astronomer Johannes Kepler, is a mathematical conjecture about sphere packing in three-dimensional Euclidean space. It says that no arrangement of equally sized spheres filling space has a greater average density than that of the cubic...
  
  .