Did the Appel/Haken graph colouring (four colour map) proof really not contribute to understanding?

Solution 1:

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?