I know it was not induction. My point is that a computer program to consider all the cases is just another mathematical tool morally similar to induction. The

I know it was not induction. My point is that a computer program to consider all the cases is just another mathematical tool morally similar to induction. The program does tell us something, namely that the problem can be reduced to a bunch of similar cases all of which are colorable. The difference is that the insight is perhaps a level removed from a normal proof. Essentially, I think that it's the program and not its output that plays the philosophical role of the proof in this case. Of course, my perception is significantly colored by the fact that I'm mainly interested in programming languages rather than traditional math :P.