
An enumeration proof is a proof that generates and then analyzes all possible cases for a problem or some aspect of a problem. If the number of cases is large, computer assistance becomes indispensable. This paper gives an example of a proof by enumeration using Mathematica. Perhaps the best example of a computer generated enumeration proof is the solution to the fourcolor map problem by Appel and Haken [AH76]. They demonstrated that four colors are sufficient to color any planar map so that no countries sharing a border will share the same color. The technique for the proof was suggested by A.B. Kempe in 1879. But, because of the large number of cases that needed to be considered, the actual proof did not appear until 1976. While worthy of study, the proof is too complex for students to attempt replicating it. The Appel and Haken proof would have taken 300 hours of CPU time on a supercomputer of that era. (Lacking access to such a machine, it took closer to 1200 hours [Kol76].) Fortunately, there are other enumeration proofs accessible to students. Such a proof, based on tangrams and using Mathematica, is given here.

