Are there human checkable proofs of the Four Color Theorem?

Kenneth Appel and Wolfgang Haken made the Four Color Conjecture into the Four Color Theorem (4CT) in 1976. Their proof, as you probably know, relies essentially on computer aided checking, which makes it not checkable by a human. Today I want to talk about their proof, the nature of computer aided proofs, and new alternative approaches to the 4CT. I also want to draw a parallel between their great achievement and some of our open problems.

I was at Yale University, in the Computer Science Department, when they discovered their proof. The Yale mathematics department quickly invited Haken to give a talk on their proof. As you might expect the room was filled, and Haken give a wonderful talk: on the history of the famous problem, on previous approaches, and on their proof.

I remember two things vividly about his visit–even though it was over thirty years ago. During the talk, he was asked what type of computer they used, since the proof required extensive computation. Today no one would probably ask this question, since the computations could be done easily on laptops. However, by 1970’s standards, the computation was huge: over 1200 hours was needed on a “super-computer”. Haken answered that he did not know what type of computer they used, but it was “blue.” That got a good laugh; in those days blue meant an IBM mainframe.

The other recollection is what Haken said to me during a private conversation I had with him, before his talk. I quickly realized that Haken, who previously had been a Siemens engineer, had a very pragmatic approach to the four color problem. To him it was more like an engineering project, then a delicate mathematical proof. One of the central issues was discovering whether certain graphs were reducible, which I will define later on. The proof required that a specific set of about two thousand small planar graphs were reducible.

What impressed me was that Haken had heuristic rules. He could look at a small graph and almost always see instantly whether or not the graph was reducible: even though the computer took a long time to actually decide reducibility. He also said that if one of the graphs later turned out to not be reducible, then he could easily find another one that would work in its place. Somehow he had “over-engineered” the proof, as you would a bridge for safety.

The Computer Assisted Proofs of 4CT

Subsequently, Neil Robertson, Daniel Sanders, Paul Seymour and Robin Thomas created a new proof based on the same basic approach as Appel and Haken, but they simplified some technical parts. There even is some belief that perhaps the “new” proof is the first complete one. The Appel and Haken proof had a number of details that were found to be wrong, and had to be fixed. They also used some technically tricky arguments that the new proof avoided.

I tend to believe that Appel and Haken have a correct proof, but I base this not on any first hand knowledge. I know Appel’s son well, he has been a professor at Princeton and has told me some details of how he helped his dad and Haken with the programming. Many times, Haken has stressed that he and Appel should not deserve full credit for solving the four-color theorem. “We did the last 20 percent,Ó he says. We were the fifth generation of people working on the problem, so four-fifths had been done by others.Ó Someone like that deserves to be right.

In any case both proofs rely on an extensive computer computation, and they both have roughly the same overall structure. As Haken says, they were just following the path that previous researchers had travelled.

The proofs of the 4CT are both inductive. Assume by way of contradiction that the 4CT is false, then let be a planar graph that is the smallest size counter-example. Let be a finite set of planar graphs, this set of graphs is cleverly chosen to have two key properties.

First, is unavoidable. This means that every planar graph has one of the graphs as a subgraph. In both proofs the size of this set is large, but not too large. For example, in the original proof the size was about , in the newer proof the size is less than half that. The proof that is unavoidable is based on a clever argument that uses the famous Euler’s relationship

for planar graphs, where are the number of edges, is the number of vertices, and the number of faces. The way that is proved to be unavoidable is based on a discharging argument, that was created by Heinrich Heesch. Roughly “charges” are assigned to the vertices of a planar graph. The charges are moved based on certain local rules: total charge is preserved by all such moves. The key is the rules eventually yield a negative charge as long as no subgraph of is in . But the charge can be shown to be positive initially by Euler’s formula, so this is impossible.

Now for the computer aided part. The set of unavoidable graphs are proved to be reducible. Roughly this means that they cannot be a subgraph of any counter-example to the 4CT. This is where the computer checking occurs. The computer needs to do an exponential calculation of all possible boundary colorings to show that these graphs are reducible. Note, it is not the number of graphs that is a problem. Checking that even one is reducible seems to be an impossible task for a human.

This implies the 4CT, since is seen not be a minimal counter-example graph.

Conventional Wisdom was Wrong–Again

One of the great achievements, I believe, of Appel and Haken was the not the proof of 4CT. It was believing that the structure I just outlined would work. The general structure of unavoidable graphs and reducibility, had already been used before them. The previous proofs were all of the following type: If a planar graph has less than vertices, then it is four colorable. Researchers believed that could be made larger and larger with greater work, but the conventional wisdom was that one could never prove that , i.e. use the method to completely solve the four color conjecture. Note, some believed that the method could not work in principle, while others believed that it could work in principle, but could not be done in practice. However, Appel and Haken “really” believed and push on, where others had stopped.

Everyone before them had used sets that came with both good and bad news. The bad news was that the set was not unavoidable, it was true that a graph could only avoid by being larger than some bound, say vertices. The good news was that the graphs in were small enough that their reducibility could be checked by hand.

The brilliance, I believe, of Appel and Haken was to believe that there would be a set of unavoidable graphs with two properties: First, that the set would be finite and unavoidable for all planar graphs, not just small ones, Second, that the graphs in the set could be checked for reducibility by computers that were available to them at the time. The search to test reducibility grows roughly exponential in the size of the boundary of the graphs. Haken told me that he had heuristic arguments that showed that he could keep the size of graphs small enough so that the computer calculation would work, yet large enough so they would be unavoidable.

The conventional wisdom at the time was mixed whether or not this approach could ever prove the 4CT for all planar graphs, but Appel and Haken believed in the method. It sounds almost silly, but sometimes problems get solved when someone believes that a method will work, where others believed it would not. This has happened over and over in mathematics; for example, the same phenomena happen with Hilbert’s Tenth problem on Diophantine Equations. More on that in the future.

I think this is a lesson for us. Is there some method that we have tossed aside, yet it can be made to work to solve P=NP?

Are They Proofs?

I was at a meeting at the Royal Society in 2004, on: What is the nature of proof? Rich DeMillo and I are (in)famous for writing a paper on the role of proof in the correctness of computer programs. I will discuss our paper another time. They invited Rich, but since he was unavailable I got to go and give a talk at the conference. In any event, I was honored to be at a Royal Society meeting. One talk was given by Robert MacPherson on another proof that is based on large computer computations and has no known human checkable proof. To quote 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?

As you might expect there was quite a lively discussion about what are proofs and is a computer assisted proof a proof? No consensus was reached by the group, but it is interesting that most (all) the heavy hitters– Michael Aschbacher, Michael Atiyah, Paul Cohen, Jean-Pierre Serre–argued against computer aided proofs. Their main point, stated strongly by Cohen, was that proofs were not to check that something is true. Rather the role of proof is to give insight into the problem at hand. A humanly understand proof can lead to additional insights, can open up new avenues of discovery. That is missing, in their opinion, in any proof that is not understandable.

I will say more about this in the future, for I think it is a fascinating issue. One that is at the core of much of what we do in theory.

Human Proofs of 4CT?

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.

Yuri Matiyasevich, of Hilbert’s Tenth Problem fame, has proved that the 4CT is equivalent to the statement that a particular Diophantine equation

has no solution in natural numbers . He has also showed that 4CT can be proved by proving certain statements about a probabilistic space on the triangulations of a sphere. The statements concern the positive correlation among pairs of events.

In the same spirit, I wish to report a new restatement of the 4CT. To my knowledge, this is the first restatement to an “Erdös-type” approximate combinatorial problem. This is joint work with three of graduate students: Atish Das Sarma, Amita Gajewar, Danupon Nanongkai of Georgia Tech.

Our Approach

Peter Tait proved in 1880 that the 4CT is equivalent to showing that certain planar graphs have edge 3-colorings. More precisely, Tait proved the following theorem:

Theorem: Let be a cubic two-edge connected plane graph. has an edge 3-coloring if and only if has a face 4-coloring.

Tait’s proof of his theorem is constructive. In modern terms he actually proves that each implication can be done in linear time.Thus, if a graph has an edge 3-coloring, then the face 4-coloring can be constructed in linear time.

Tait used his theorem to claim a “proof” of the 4CT. He assumed that every two-edge connected cubic planar graph has a Hamiltonian tour.This assumption is unfortunately false as shown years later, in 1946, by William Tutte: there are such planar graphs without any Hamiltonian tours. Note, the existence of such a tour easily proves that the graph is edge 3-colorable. The proof of this is simple: Color the edges of the tour alternatively red/green. Color all other edges blue. It is easy to see that this is a valid edge 3-coloring of the graph. Note, the reason this works is that a cubic graph must have an even number of vertices. Our approach to the 4CT is this:

Theorem: If every two-edge connected, cubic, planar graph can be edge 3-colored with errors, then the Four Color Theorem is true.

By a 3-coloring with errors we mean an assignment of 3 colors to the edges of the graph so that at most vertices have two edges of the same color. Thus, the theorem says that we can strengthen Tait’s theorem to allow errors, where is the number of vertices.

The hope, that we have made no progress on yet, is that there is a clever combinatorial argument that colorings with few errors always exist. We think that allowing errors in the coloring could allow powerful tools from modern combinatorics to be applied to the 4CT. We will see.

In the our theorem we regard the four color theorem as a conjecture (otherwise, the theorem statement is trivial). One way of looking at our theorem is we ask for a proof of the fact that every two-edge connected cubic planar graph , on vertices, can be decomposed into a union of disjoint cycles covering all vertices, with at most odd length cycles. If such a decomposition exists, we can color the edges on every cycle with red and green alternatively, and color all other edges with blue. This way, there will be at most errors. In fact, we do not even need a cycle cover, it is sufficient to have a cover of paths and cycles with paths and odd cycles. This is a weaker requirement than Tait’s, as he needed a Hamiltonian tour.

For the full details of the proof see our paper. However, the basic idea is based on an amplification “trick”. Suppose that is a two-edge connected, cubic, planar graph that cannot be 3-edge colored. We will take copies of and glue them together to form a new graph .

The gluing together yields a two-edge connected, cubic, planar graph. By assumption it has an approximate 3-edge coloring with at most

errors. For large enough , we get that one of the copies of is colored with no errors. However, there is a small problem, the subgraph that is a copy of has been modified: it has extra vertices and edges. These were added so it could be connected to other copies of . Thus, the last step is to show that this can be overcome. We finally, get a 3-edge coloring of , which is a contradiction.

Open Problems

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.

Another question is to make the known computer proofs human proofs. The issue is the reducibility step needs to be made humanly checkable. A way to do this, at least in principle, is to show that checking whether a graph is reducible or not is in NP. Then, we could use the computer to generate a short proof that we could check by hand.