I hope this isn't off topic – sorry if I'm wrong.
In 1976, Kenneth Appel and Wolfgang Haken proved the claim (conjecture) that a map can always be coloured with four colours, with no adjacent regions given the same colour. This was controversial because the proof process required a computer to evaluate many different cases.
From what I've read, the controversy was (1) that no human could reasonably confirm the proof, and (2) that being a computer proof, all it did was give a yes/no answer to the question – it didn't contribute to the understanding of the problem.
The first issue seems to be a non-issue now – the proof has been replicated using different software. But the second issue seems to stand – and I don't really understand that issue.
Quite a few proofs require a number of particular cases of the problem to be separately checked. Having eliminated every possible case where the answer might have been "no" is a routine way of proving that the answer is "yes". Does it really make any difference in principle whether the number of cases is 2 or 2 million? Does the scale of that number make any difference to the degree of human understanding of the problem?
And, given that people wrote the software that evaluated all the cases, all the ideas underlying the proof seem to be understandable by, and to have been understood by, people.
To me, having evaluated a thousand different variations on the same kind of a problem shows no more understanding than evaluating one. Solving a thousand quadratic equations, for instance, is much the same as solving one – all the repetitions are just plugging different numbers into the same formula, or repeating the same completing-the-square procedure, or whatever.
Therefore, I am very much impressed that Appel and Haken were able to understand the problem in sufficient depth that they could write a program to derive what all the special cases are and check them. Writing software to reliably determine all the cases often shows even deeper understanding than manual derivation of all the cases, where deeper understanding can be bypassed to a degree by trial-and-error.
Getting the computer to run the program, once written, seems irrelevant to me. The program presumably could have been (eventually) executed by a person, in the same way that it could have been executed by a Turing machine, but doing the mechanical follow-the-steps stuff seems irrelevant to depth of understanding.
Is there something I'm missing?
Best Answer
When people say that Appel-Haken did not really contribute understanding, they aren't necessarily talking about the four-color problem itself. They mean that the proof did not really contribute any understanding of mathematics.
A famous example when the proof of a long-standing conjecture really did contribute a lot of understanding is Andrew Wiles' proof of Fermat's Last Theorem. People weren't excited about this proof because they cared directly about the answer to FLT; they were excited because the proof brought together and integrated ideas from many disciplines and represented progress on the much larger Langlands program. Similarly, Perelman's proof of the Poincare Conjecture introduced important new ideas and tools. This was why many experts were convinced that Perelman's proof was valid even before it was formally checked; the high-level summary contained enough nontrivial ideas that they already saw that there was something extremely interesting going on.
In other words, the problem with Appel-Haken is that it is boring. It was more or less an application of an already-understood technique, just on a larger scale, and so has led to very little interesting new mathematics. People are still looking for a conceptual proof of the Four-Color Theorem analogous to the two proofs above, for example people working in quantum topology; see this blog post by Noah Snyder and Kainen's Quantum interpretations of the four-color theorem. A proof along these lines would be much more interesting, as it would likely shed light on a number of other issues in quantum topology.
This principle applies to more than just long-standing open problems. Many problems you might encounter in an undergraduate course might be solvable by a tedious computation along the lines of the Appel-Haken proof, but often there exist much more interesting conceptual proofs along the lines of Wiles' proof. If you stopped after finding the tedious calculation you might never find the conceptual argument, which often turns out to be much more interesting (e.g. it naturally suggests generalizations, interesting concepts, ties to other branches of mathematics...).
I will take your comment about quadratic equations as an example. It's true that the quadratic formula allows you to solve quadratic equations mechanistically. The question, then, is whether the quadratic formula leads to any significant conceptual understanding of polynomials. For example, does it suggest a natural route to the cubic formula?
If you think of the quadratic equation in terms of completing the square, then you quickly run into a problem: you cannot, in general, complete the cube. So completing the square does not generalize to cubic equations. If you want to understand cubic equations, it follows that you need to think about the quadratic formula more conceptually.
The conceptual breakthrough is the following: what the quadratic formula really shows you is that there is a symmetry to the roots of a quadratic polynomial. The roots
$$x_1 = \frac{-b + \sqrt{b^2 - 4ac}}{2a}$$
and
$$x_2 = \frac{-b - \sqrt{b^2 - 4ac}}{2a}$$
are conjugate: they are related by a symmetry which flips the sign of the square root. This symmetry manifests itself concretely in the fact that the sum
$$x_1 + x_2 = - \frac{b}{a}$$
is completely invariant under flipping the sign of the square root, whereas the sum
$$x_1 - x_2 = \frac{ \sqrt{b^2 - 4ac} }{a}$$
is completely negated under flipping the sign of the square root. Taking this idea seriously leads you to the method of Lagrange resolvents, and now if you were born in the right century you would be well on your way to inventing group theory, Galois theory, and (if you were really observant) representation theory.
Isn't that way more interesting than using the quadratic formula?