Notes found on internet on why a non computer proof of this problem is important or not important. I tried to collect all the notes I found (other will follow), no matter the different opinions I may have on the subject:

**Robin Thomas**: “We should mention that both our programs use only integer arithmetic, and so we need not be concerned with round-off errors and similar dangers of floating point arithmetic. However, an argument can be made that our `proof’ is not a proof in the traditional sense, because it contains steps that can never be verified by humans. In particular, we have not proved the correctness of the compiler we compiled our programs on, nor have we proved the infallibility of the hardware we ran our programs on. These have to be taken on faith, and are conceivably a source of error. However, from a practical point of view, the chance of a computer error that appears consistently in exactly the same way on all runs of our programs on all the compilers under all the operating systems that our programs run on is infinitesimally small compared to the chance of a human error during the same amount of case-checking. Apart from this hypothetical possibility of a computer consistently giving an incorrect answer, the rest of our proof can be verified in the same way as traditional mathematical proofs. We concede, however, that verifying a computer program is much more difficult than checking a mathematical proof of the same length.”**Martin Gardner**: “Whether a simple, elegant proof not requiring a computer will ever be found, is still an open question. It’s interesting that such a simple, intuitive puzzle can be so difficult to settle!”**Teena Andersen**: “Until an easily understood proof can be found (a proof without the aid of computers), the Four. Color Theorem remains a heuristic that represents a “Holy Grail” for many mathematicians.”**Sarah Buchan, Sharvari Nadkarn**: “Even now, the proof is complicated and requires a computer – not so nice and neat as mathematicians would like”**MacTutor History**: “The Four Colour Theorem was the first major theorem to be proved using a computer, having a proof that could not be verified directly by other mathematicians. Despite some worries about this initially, independent verification soon convinced everyone that the Four Colour Theorem had finally been proved. Details of the proof appeared in two articles in 1977. Recent work has led to improvements in the algorithm”**Andreea S. Calude**: “Its computer aided proof has forced mathematicians to question the notions of proofs and mathematical truth.”**Herald Gazette Scotland**: “Your own maths theorem for £15. Pythagoras spent his life proving his, and Fermat died still trying – but for the would-be genius today, a mathematical theorem is only a mouse-click away.”**Devlin’s Angle (MAA)**: “A final thought to leave you with as we start a new year. To this day it is not known if there can be a short proof of the Four Color Theorem that a human could follow. Most mathematicians think there is not. But who knows?”**Edward R. Swart**: “In response to criticism of the computer-dependent proof (as a posteriori justification) of the four-color problem, this article argues that it is reasonable to regard all mathematical truths as a priori, no matter how they are arrived at. In doing this the author introduces a new mathematical entity intermediate between a conjecture and a theorem.”**Heinz Kröger**: “With Appel’s and Haken’s proof in 1977, one of the big problems was for the first time solved by means of computer programs. This approach was rather unusual at that time, a classical proof with pencil and paper is also in this case still longed for. However, checking a great number of cases in a reasonable time seems to be only possible by computer support.”**Robert MacPherson**: “In 1609, Kepler made a beautiful conjecture about spheres in space. It was one of the oldest unsolved problems in mathematics. In 1998, Tom Hales produced a brilliant computer-assisted proof of the Kepler conjecture. By now, the theoretical part of Hales’ proof has been refereed as usual mathematical papers, but the parts involving the computer have resisted all efforts at checking by humans. Should we think of the Kepler conjecture proved?”**Dick Lipton**: “As you might expect there continues to be considerable interest in finding a proof of the 4CT that does not use any computer search. Even recently, new restatements of the theorem have been discovered. … There are several open questions. The main one is to find a non-computer based proof of the 4CT. Either use Matiyasevich’s approach, or our approach, or one of your own; but make it humanly checkable.”**Ibrahim Cahit**: “Mathematicians would like to see the reliance on the computer in the proof reduced.”**Joshua Cooper**: “It’s interesting. It really gets to the heart of a current debate in mathematics: whether computer-assisted proofs are proofs or not. It’s been going on since Appel and Haken produced their proof in 1976 of the four-color theorem. That showed that any map can be colored with four colors without any two adjacent countries getting the same color. It’s been a source of debate ever since, because although there’s a lot of graph theory and other mathematics that went into the proof, the majority of the argument is just a huge computation. So the four-color theorem, according to some people, is still unproven, because there isn’t a human-readable proof of it.”**Natalie Wolchover**: “As computers grow more powerful, the issue Thurston raised is bound to come to a head: When a computer employs the axioms of logic to deduce mathematical truths that are beyond the reach of human deduction (and this now happens), should we accept these truths as proven theorems, or is proving them ourselves the whole point? Will this question divide mathematicians into two camps?”**Evelyn Lamb**: “It was the first major theorem to be proved using a computer, and for some people, it raised questions about what it means to prove a theorem. Did this computer proof count? Were mathematicians going to be obsolete soon? People are still debating the role of computers in mathematical proof and the future of mathematics as a human endeavor”-
**Underwood Dudley**: “The four-color conjecture was easy to state and easy to understand, no large amount of technical mathematics is needed to attack it, and errors in proposed proofs are hard to see, even for professionals; what an ideal combination to attract cranks!” **Justin Mullins**: “The search for an elegant proof of the Four Colour Theorem is ongoing. And while computer-aided proofs have begun to gain acceptance, largely thanks to the Four Colour Theorem, there remains the feeling that beauty, elegance and insight should triumph over the horror of a computer-generated proof”**Doron Zeilberger**: “My second 20th-century favorite was not considered worthy of mention by Atiyah, even not in a derogatory way. It is Ken Appel and Wolfgang Haken’s GORGEOUS proof of the Four-Color Theorem. Few people are aware that it is really a ONE-LINE Proof: ‘The following finite set of reducible configurations, let’s call it S, is unavoidable’. The set S itself does not have to be actually examined by human eyes, and perhaps should not. The computer would be much more reliable than any human in checking its claim. The human challenge was to design algorithms for constructing the set S. Right now we still need (human) IDEAS to find such algorithms, but not for ‘explaining’ ‘why’ four colors suffice. FOUR COLORS SUFFICE BECAUSE THE COMPUTER SAID SO! Four Colors suffice for the same reason that the speed of light is what it is, and the 1001005th digit of Pi is what it is, it is contingent rather than necessary knowledge. So The Ugly Duckling of the Appel-Haken proof was just ahead of its time, and very soon will turn into a Beautiful Swan, as our tastes and priorities will change, and we will get rid of the narrow-minded, micro-managing human trait of trying to ‘understand all the details’, and our obsession with ‘elegant proof’, that is but a euphemism for ‘trivial proof'”**Mark Walters**: “In Map Coloring, Polyhedra, and the Four-Color Problem, David Barnette guarantees that these efforts have not been wasted. He points out that many advances in graph theory were made during the process of proving the Four-Color Theorem. These advances provide justification for the 150+ years spent proving a theorem with rather useless results [BAR]. In this paper, the historical progress of the Four-Color Theorem will be examined along with the work of some of its contributors”

What I think:

- I personally do not understand why there isn’t an entire army of mathematicians trying fulltime to find a classical and elegant proof of this problem

I believe these few paragraphs by Justin Mullins are among the most eloquently written on the four-color theorem:

http://www.justinmullins.com/four_colour_theorem.htm

In particular, the last paragraph deserves to be added to your list of quotes above.

LikeLiked by 1 person

The proof they found is not a “computer-generated proof” but a “computer-verified proof”. The path to find the solution, even though very long because of the large number of conditions to test, has been found by humans .. and so far is the only one that we have 😦

LikeLike