Image: “Joseph Kosuth, Four Colors Four Words, 1966,” by Andrew Russeth, on Flickr.

 

(A continuation of Trees, Dictionaries, Pickles and Loops: Part II.)

We’ve discussed how math uses computer science for conjectures and for visualization. Those might seem like less than crucial roles. But computers are also used in proofs.

Last year I wrote about the role of proofs in mathematics. A mathematical proof is a strict logical argument. A proof of a mathematical idea shows that, according to logic, the idea absolutely must be true.

In math, proofs are fundamentally important. Many times, an idea is considered next to worthless until it’s proven.

What if I told you I had a valid proof of a mathematical idea, but it was so complicated no human being could ever read all of it? Should the idea count as proven?

Enter the Four-Color Theorem.

The Four-Color Theorem says that if you want to color in a map — any map — so that no two adjacent territories have the same color, you will never need more than four colors.

Here is the contiguous United States four-colored:

But what if I drew some crazy states, with super-wiggly sides or long pointy edges? How do you know that no matter what map I draw, you can color it in with just four colors?

No one has ever successfully come up with a short, simple proof of this fact, though occasionally people still try. It was proven in 1976 by Kenneth Appel (a Queens College alum, by the way) and Wolfgang Haken.

The catch: they used a computer. The proof is so long that no human can ever check it.

Georges Gonthier writes that the proof “combined a textual argument, which could reasonably be checked by inspection, with computer code that could not. Worse, the empirical evidence provided by running code several times with the same input is weak, as it is blind to the most common cause of ‘computer’ error: programmer error.”

In short, to trust Appel and Haken’s proof, you have to trust that their computer program worked correctly. People are not necessarily happy about this kind of trust. A University of Illinois article discusses some reactions to the proof: “When Haken and Appel announced their proof of the theorem in 1976, some greeted it with enthusiasm and others with scorn. […] To purists, you must be able to check a proof by hand, which is not possible with the computer. If you were to put the computer’s proof on paper, it would number millions of pages.”

Perhaps, the worry goes, once a physical machine is brought into the mix, a mistake could seep through the cracks.

As computers– and the people who program them– get better and better, this concern seems to be falling out of fashion. My professors certainly refer to the Four-Color Theorem as proven.

There is one other reason computer-assisted proofs can be controversial. That reason has to do with what proofs are for in the first place.

One idea is this: Mathematicians want to prove things, not just to make sure they are true, but also to understand them more deeply. The value of a proof, computer-assisted or otherwise, lies in how much it helps us to understand mathematics.

There is a fantastic discussion on Math Stack Exchange about the subject. I encourage you to take a look at it, but here are a few snippets.

1. “What is a proof for? Often we pretend that the reason for the proof is so that we can be sure that the result is true. But actually what mathematicians are looking for is understanding.”
2. “The veracity of a conjecture is often less important than the techniques required to demonstrate it. We could, for instance, happily assume the Riemann Hypothesis is true […]. Yet doing so does nothing to enhance our understanding of it.”
3. “Some people may claim that there is doubt about a proof when it has been proved by computer, but I think human proofs have more room for error. The real issue is that (long) computer proofs (as opposed to something simple like checking a numerical value by calculator) are hard to keep in your head.”
4. “The dichotomy between computers / not computers is a very false one: if we do our business correctly, we can use computers to make many (I won’t say “most” or “all,” but who knows what the future will bring) of our arguments more reliable.”

What do you think? Do computers contaminate mathematics? Is a well-constructed computer proof just as good as a pencil-and-paper one? And is there another facet to this discussion that hasn’t been mentioned?