Written: Feb 25, 2003
In a fascinating public lecture at Princeton University, given on the evening of Feb. 13, 2003, Noga Alon mentioned that it would be nice to give a purely "human", computer-free proof of the Four Color Theorem (4CT) , because it is very difficult, in fact, impossible, for a human to follow a computer-proof, and a human proof would enhance our understanding.
I completely agree that it is important to keep trying, very hard, to find a non-computer proof for 4CT, but not for Noga's reasons! I understand the 4CT theorem perfectly. It is really a one-line proof modulo routine-checking. It asserts that a certain set of reducible configurations is unavoidable. It only takes a few minutes to understand the definitions, and to convince oneself that the existence of such a set implies 4CT. Analogously, to understand a computer proof that a certain 400-digit integer is composite all one has to do is to grasp that if it is a product of two smaller integers both greater than 1, then it is indeed composite. I don't know and I don't care how the computer found the factorization, and I believe that it can multiply two integers and check the claim.
So unless Factorization is in P, we have lots of potential genuinely `deep' results. But deep as they are, they are kind of boring. Wouldn't it be nice if they were examples from real mathematics, that are genuinely deep.
There is hope. Goldbach, RH, lim R(n,n)^(1/n)<3, etc., may be really deep. But, we don't know that. On the other hand, FLT, and all other human-proved theorems are shallow, since they were proved by humans, without the aid of computers.
I very much hope that 4CT is not humanly-provable, since this is my pet-candidate (along with Kepler's ex-conjecture) for a known, interesting, and deep result. In principle, it might be possible to meta-prove a lower-bound for the complexity of the shortest proof of 4CT, but, unfortunately, this seems to be orders-of-magnitude yet harder than 4CT, and, like the P vs. NP problem, will probably resist both human and computer efforts.
The next best thing to a formal proof that 4CT is really deep is a sociological test. If humans will keep trying to find human proofs, and fail, it will raise the probability that 4CT is indeed deep. On the other hand, if some human will prove 4CT tomorrow, only with pencil-and-paper, then this would be very nice for the prover, who will become instantly famous, but very depressing for our mathematical culture as a whole. It would mean that perhaps we humans are so trivial that we are not even capable of stating and conjecturing deep results.
Hence my reasons for encouraging human proofs are really Popperian. Karl Popper said that it is always very important to try and refute the prevailing theory, and we, as a whole, should hope that these attempts will fail, since it is traumatic to give up our cherished theories. Sure enough, the refuter would be happy, but the rest of us should hope that the repeated attempts will fail, since these failures increase our confidence in our theories.
So, go ahead Girls and Boys, don't give up and keep on trying to find a "proof from the book" to 4CT, or at least a human-readable one! I wish you good luck, but deep in my heart, I hope that you would fail!
Read the interesting comments by Noga Alon and Yair Caro and Yavor Iliev (received June 10, 2003), and the deep and thought-provoking essay, by Tim Gowers.
[ADDED JAN. 12, 2023: I am happy to report that this paper was retracted]