Admittedly, dealing with only a finite number of elements seems hardly useful, as we mostly want results that apply generally, and not specifically. Here, we provide a contrived example simply to demonstrate the technique.

We could perhaps call the result derived in Example 3.6.1 a theorem since we did provide a proof for the fact, but we prefer to reserve the term theorem for “major” results. The result in Example 3.6.1 was merely an exercise.

Based on Example 3.6.1, we can see why the method presented in this section is called the Method of Exhaustion: it is because we exhaustively check every single element in the desired set for a desired property. Note that while the term exhaustion is used to describe the thoroughness of checking every element, it does not necessarily refer to the feeling one may get whilst performing the checking, though it should be said for rather large sets, this method can be tiresome.

Let’s lay out the argument in logical fashion, same as we’ve done before. The reason this method works is because we verify that every element in the desired set has some desired property.

Suppose set A is a finite subset consisting of the n elements

A = {a₁, a₂, a₃, …, a_n}

taken from some universal set 𝒰. Furthermore, suppose p is an open statement defined on 𝒰. The Method of Exhaustion is simply an argument of the form

That’s all there really is to it.

Just because a set is finite does not mean it is feasible to hand-check every single element within it. Sometimes, tasks can be automated by writing computer programs to check thousands or even millions of elements in a timely fashion.

While the example represented here was rather contrived, one major result proved using the Method of Exhaustion was the Four Color Theorem. For centuries cartographers have been making maps of various places around the world, and one way to draw maps is to color regions so they are easily distinguishable. However, it is typically expected that adjacent regions on a map are colored differently, helping them stand out visually.

It was shown at some point in the late 1800s that no more than five colors were needed for any map so no adjacent regions shared a color, but it was suspected that no more than four colors were needed as well. Though many mathematicians attempted to prove that no more than four colors were needed, many efforts proved fruitless.

Progress marched forward in the 1960s with the advent of computing technology. Two mathematicians Kenneth Appel and Wolfgang Haken further developed results derived from Heinrich Heesch to complete a proof. Essentially, one major step in the proof was showing that all maps could be “reduced” to a small number of essential configurations (basically, all maps are basically distortions of some simpler underlying map that represent the same types of regions.) Appel and Haken found that there were only 1834 configurations.

Once Appel and Haken found these configurations, it was simply a matter of checking each and every single one (using the Method of Exhaustion.)

This proof was the first major proof to be verified by computer. As such, it was a controversial result: not all mathematicians readily accepted the proof because it was hard and time-consuming for a human to check.

Nevertheless, the proof has mostly withstood scrutiny, with a minor error being corrected by Appel and Haken sometime in the late 1980s.

This Wikipedia article offers a more complete look at the history of the theorem, as well as additional resources one can look into for more information.

The point is while the Method of Exhaustion may seem overly simple and contrived, being restricted to only finite sets instead of infinite sets, it is still a valid proof technique that can come in handy.