MJackson.Wbst@PARC-MAXC.ARPA (03/07/84)
By "planar map" in my previous message I meant to connote a structure on a two-dimensional surface, not strictly a flat plane. In fact, the plane and the sphere are topologically equivalent (the plane is a sphere if infinite radius) so four colors suffice for both; for the torus, which has a different "connectivity," it has long been known that seven colors are both necessary and sufficient. I'm not a mathematician but at one time (right after reading an article) I felt as if I understood the proof. As I recall it is based on the fact that if there are any maps that require five colors there is a minimal (smallest) map that requires five colors. It is possible to construct sets of graphs (representing map regions) of varying complexity for which any map must include at least one member of the set. It is also possible to determine for some particular graph whether it can be "reduced" (so that it represents fewer regions) without altering its four-colorability or its interactions with its neighbors. Clearly the minimal five-color map cannot contain a "reducible" graph (else it is not minimal). Evidently, if one can construct a set of graphs of which ANY map must contain at least one member, and show that EVERY member of that set is reducible, then the minimal five-color map cannot exist; hence no five-color map can exist. Now if it were possible to construct such a set with, say, 20 graphs one could show explicitly BY HAND that each member was reducible. No one would call such a proof "ugly" or "not a true proof;" it might not be considered particularly elegant but it wouldn't be outside the mainstream of mathematical reasoning either (and it doubtless would have been found years ago). The problem with the actual case is that the smallest candidate set of graphs had thousands of members. What was done in practice was to devise algorithms which would succeed at reducing "most" (>95%?) reducible graphs. So most of the graph reduction was done by computer, the remaining cases being done by hand. (I understand that to referee the paper another program had to be written to check the performance of the first.) I would like to hear any criticism of the Illinois proof that is more specific than "ugly" or "many feel that this does not constitute a true proof." A pointer to the mathematical literature will suffice; my impression is that the four-color theorem is widely accepted as having been proved. (We may be getting a bit far afield of AI here; I would say that my impression of the techniques used in the automatic reduction program was that they were not "artificial intelligence," but since they were manifestly "artificial" I hesitate to do so for fear of rekindling the controversy over what constitutes "intelligence!") Mark
WILKINS@SRI-AI.ARPA (03/08/84)
From: Wilkins <WILKINS@SRI-AI.ARPA> I am not familiar with the literature on the 4-color proof, nor with whether it is commonly accepted. I do however have a lot of experience with computer programs and have seen a lot of subtle bugs that do not surface 'til long after everyone is convinced the software works for all possible cases after having used it. The fact that another person wrote a different program that got the same results means little as the same subtle bugs are likely to be unforeseen by other programmers. If the program is so complicated that you cannot prove it or its results correct, then I think the mathematicians would be foolish to accept its output as a proof. David