# Example of why proof by exhaustion is inelegant

There's a nice example of why people dislike proof by exhaustion on the Wikipedia page. The problem statement is "prove that all years in which the Modern Olympics are held are divisible by 4". One can prove this by induction by showing that the first year, 1896, is divisible by 4, and applying the fact that all Olympic games are 4 years after the previous one. Alternatively one can prove this by exhaustion by listing out all the years in which Olympic games were held, and checking that they are all divisible by 4. Naturally the first method is preferable, not only because it's simpler, but also because it proves the statement indefinitely into the future.

Only problem with this is that there's going to be an Olympic Games in 2021 thanks to COVID, and 2021 is not divisible by 4.

What is a good replacement for this example? The obvious thing is to choose some well-known, reliably repeating event, but it's not easy to think of something that isn't annual. There is Halley's Comet, but the period of that is not a nice round number (75.32 years).

NB: I notice the Wikipedia article has changed to specifically exclude the 2021 Olympics, but the more exceptions are listed (the cancelled Olympics during WW1 and WW2 are already listed) the less elegant the example becomes, too.

• How about the football world cup? May 12 '21 at 7:25
• Is the phrase "proof by exhaustion" used in this context? I have only heard it used in the context of Archimedes' proofs, which are much like taking a limit. May 12 '21 at 14:29
• @Sue VanHattum: Now that I think about it (from reading your first comment), it does occur to me that "proof by exhaustion" usually means the Archimedes method (which I think actually originated with someone earlier, but Archimedes was by far the most expert in the method back then). However, I have heard this term used in the present sense, but I've heard the phrase "proof by cases" much more often. Perhaps people say "exhaustion" when the case-by-case analysis is lengthy and tedious, and say "cases" when the analysis is something like whether a number is positive, negative, or zero. May 12 '21 at 14:47
• @SueVanHattum I remember a remark in a textbook that proof by exhaustion is so-called because it exhausts (i.e. tires out) the prover, which I personally also find is a neat comment to add. May 13 '21 at 2:16
• "it's not easy to think of something that isn't annual.": How about $17$-year cicadas? May 13 '21 at 23:12

Again, the more standard label would be "by brute force" or "case by case", rather than "by exhaustion", since the latter refers to a proto-calculus method dating back at least to Archimedes.

My own reaction to lengthy case-by-case treatment is that such a discussion seems to give no reason for the phenomenon. That is, a "good explanation" hopefully/presumably encompasses the various seemingly-special reasons that work in the possibly myriad "cases".

Sometimes the trade-off is dubious: some results about semi-simple real Lie groups are just basic linear algebra for the classical groups, but intrinsic (=case-independent) arguments often require much more, and are not necessarily illuminating ... especially with regard to classical groups (such as $$GL_n(\mathbb R)$$).

• FWIW the Rosen Discrete Mathematics book I use (8E, 2019) does call this "proof by exhaustion" and not anything else. May 15 '21 at 4:19

Perhaps equally interesting are theorems that can only be proved "by exhaustion"---by a long case analysis---as far as we know. For example, that there are only a finite number of sporadic simple groups seems to be such a theorem. According to Jack Schmidt, Gerhard Michler studied the issue and thinks that "it should not be taken for granted that there are only finitely many sporadic groups": there is a natural procedure to possibly generate an infinite number. But it doesn't.

Another example, closer to home, suggested by @user52817 in a comment. In an MO question, I asked which unfoldings of the hypercube tile $$3$$-space. My question was recently answered by Moritz Firsching, using integer programming: All $$261$$ unfoldings of the hypercube tile $$3$$-space! But the proof is by exhaustion of the $$261$$ cases; no overarching theorem is known. This raises the question:

Q. Is it true that, for every $$d$$, each of the unfoldings of the $$d$$-dimensional cube tiles $$\mathbb{R}^{d-1}$$?

We now know this is true for $$d=3,4$$: The $$11$$ unfoldings of the $$\mathbb{R}^3$$ cube tile $$\mathbb{R}^2$$, and the $$261$$ unfoldings of the $$\mathbb{R}^4$$ hypercube tile $$\mathbb{R}^3$$.

• Another example which was proved by essentially "a long case analysis", with it being so relatively extensive a computer program was used instead of it being done by hand, is the Four color theorem. May 14 '21 at 0:31
• @JosephOfRourke-you should write an answer that describes your work with unfolding hypercubes. The methods seem to involve exhaustively checking many cases, with very interesting end results! May 15 '21 at 16:12
• @user52817: Good point. Added, and posted a corresponding MO question. May 15 '21 at 23:49

A classical example of proof by exhaustion is to establish an integer $$N$$ is prime by trial divisions. One uses trial division by candidates for divisors up to $$\sqrt{N}$$. This can be made slightly less exhausting by using the method of the Sieve of Eratosthenes.

If $$N$$ is large, say 250 digits, then this approach to establishing primality is not practical, even with a computer. There are algorithms for primality testing that are much more efficient but they do require some theory beyond the brute force "method of exhaustion" approach. For this sort of reason, the method of exhaustion is sometimes deemed "inelegant." "Elegance" would be to develop or learn some theory to approach the problem smartly.

The method of exhaustion takes an interesting turn when the number of possible cases to check is infinite. For example, we might try to prove there is an odd perfect number by starting with 3 and working until we find an odd perfect number $$2n+1$$. People have tried this approach to no avail. Perhaps there will be an elegant theoretical advancement some day that proves there are no odd perfect numbers. Or perhaps a quantum computer will find an odd perfect number some day. Or perhaps the problem will be unsolved forever!

There are arithmetic statements $$P(n)$$ which are false for every $$n\in{\bf N}$$ but which are independent of standard systems of axioms. The statement $$[\hbox{for all }n: P(n)]$$ would have neither a proof nor a counterexample. Therefore to establish such a statement $$P(n)$$ is always false would require the method of exhaustion to check for every case $$n$$, which is not possible in finite time. I guess these arithmetic statements get the last laugh!

Nearly every classical or recreational math result about a finite set is an example.

Can we have a walk in Königsberg so as to cross each of its seven bridges once? Well, we can attempt starting at southeast point then cross northward then cross back then go east... Never mind, Euler had a better approach.

Can we tile a chessboard with A1 and H8 removed by $$1\times 2$$ tiles? Well, we can try placing the first domino to A2A3 then second to A4A5 ... But it is easier to notice that we have removed two black squares.

Can we decompose 1087 into a sum of two squares? We can try 1+1086 or 4+1083 or 9+1078 etc. and check that none of the second terms is a square, or we can notice that an odd sum of two squares equals 1 modulo 4, and 1087 equals 3.

Prove that all popes had less than 150 years when they died.

You could look at each of 260 of them and verify that this holds.

Or you could take the fact that the oldest known person lived up to 122 years, which can be used to automatically conclude that all popes can only be less than this.