Coloring general graphs is, as I said in my last post, quite difficult. But if you can restrict the structure of the graph, you can change the problem in a way that makes it *much* easier. The classic example of this is *planar graphs*.
A planar graph is a graph which can be drawn on a plane with no edges crossing. Every planar graph is also the structural equivalent to a map, where the vertices corresponding to two countries on a map are adjacent if and only if the countries share a border in the map. (A border here has non-zero length, so two countries that only meet in a corner don’t share a border.) You can see an example of a map with its corresponding planar graph overlayed to the right.
In the late 19th century, it was proven that any planar graph could be colored with only five colors. (Actually, it was an *attempt* to prove that any planar graph could be colored with only four colors, but the proof contained an error; after correcting it, it could only show that you could color a planar graph with no more than 5 colors.) Not only that, but exploiting the properties of a planar graph, you can 5-color a planar graph in *linear* time.
People were pretty much sure that it was true that every planar graph could be
four-colored, but every attempt to prove it failed. The work that led to the eventual
proof was based on the idea of looking at the failed proofs, examining the cases that
they missed, and figuring what a counterexample of the 4-color theorem would look like. For example, there’s a result along the way called the *snark theorem*, which defines an interesting kind of graph which could potentially be a basis for a counterexample.
(Calling this kind of graph a snark, and the theorem the snark theorem is a relatively recent thing; but it’s now pretty widely used.)
A snark is a graph with the following properties:
1. It’s connected: there is a path from any node in the graph to any other
node in the graph.
2. It’s *bridgeless*: there is no single edge that will split the graph
into two disconnected subgraphs if it’s removed.
3. It’s *cubic*: every node has three edges.
4. It has chromatic number 4: it can’t be colored in less than 4 colors.
The snark theorem says that the four-color theorem is *equivalent* to the
statement that no snark is planar.
The work to find a counterexample never managed to find one. Finally, in 1976, Andrew Appel at UIUC came up with a proof of the 4-color theorem: it seemed to work, but it was
(and in fact still is) rather controversial. The idea of it was to define the properties of any graph that could form a counterexample. This produced a collection of close to 2000 graphs in the original version, which were called *unavoidable* graphs, because any minimal counterexample to the 4-color theorem needed to include at least one of them as a counterexample. (They later managed to reduce that set to 1476 unavoidable graphs.) The
collection of unavoidable graphs was generated by a computer program, and then the resulting set of graphs was 4-colored. So they exhaustively showed that every possible
counterexample to the 4-color theorem was 4-colorable. (You can see a more modern version
of the proof based on a set of 633 unavoidable configurations [here][thomas].)
[thomas]: http://www.math.gatech.edu/~thomas/FC/fourcolor.html
The big reason for the controversy was that THE proof was over 500 pages long, and
relied on an extremely complicated algorithm to produce the unavoidable graphs. No one could really hold the entire thing in their head, and no one could
manually reproduce the results. This meant that accepting the correctness of the proof came down to accepting the correctness of the program that generated it – and in fact, not just the correctness of the program, but the correctness of the compiler and the hardware than ran it. And that was, and still is, not at all a popular idea.
It’s also considered by many purists to be *ugly*. The common quote about it (and I haven’t been able to find a definitive source for who first said it) is: “A good proof is like a poem; this beast is more like a telephone book.”
But the fact remains that it seems to be true. It’s been reproduced by multiple people
using multiple independently written programs; the number of cases has been pared down
considerably; and pretty much everyone agrees that it’s true, even if the proof is not
exactly loved.
People have also written 4-coloring algorithms, which are reasonably efficient. Given a planar graph, you can 4-color it in quadratic time. Quadratic isn’t great, but it’s a far cry better than exponential.
This proof will become uncontroversial the day we can bust out the nanotech pixie dust and upload our minds into computers.
After three years from the announcement of my proof “Spiral Chains: A New Proof of the Four Color Theorem” (http://arxiv.org/abs/math/0408247) all comments and critics have been answered therefore I would say that the proof of 4CT by using spiral chain is an alternative non-computer proof.
I. Cahit
The proof of 4CT was achieved by *Kenneth* Appel and Wolfgang Haken (with J. Koch). Andrew Appel is Kenneth Appel’s son.
I’m pretty sure that snarks are supposed to have edge chromatic number 4, not (vertex) chromatic number 4…
A snark is a graph with the following properties:
1. It’s connected 2. It’s bridgeless 3. It’s cubic 4. It has chromatic number 4
Wait a minute! Snarks are supposed to have FIVE unmistakable marks!
And that is the fifth unmistakable mark. Asked and answered. 😉
Thanks for this post, Mark! I read about this proof years ago, but had never been able to feel that I understood what the issues were.
I probably don’t understand much better now, but I feel as though I do! 🙂
(WARNING: long post. Sorry).
micah’s right: A Snark has chromatic index (that is, edge-coloring number) 4.
Two further comments on the overview of the proof:
1. The description is slightly misleading. The set of unavoidable configurations is not a complete set of potential counterexamples that need to be 4-colored. Rather, it is a set of subgraphs that every planar graph must contain. There are many such sets, some of which contain very few configurations. For instance, every planar graph must contain a vertex of degree at most 5 (this is an easy consequence of Euler’s formula), so “vertex of degree 2”, “vertex of degree 3”, “vertex of degree 4” and “vertex of degree 5” forms a set of four unavoidable configurations.
The trick is to find a set of unavoidable configurations each of which is *reducible*. Being reducible does not mean being 4-colorable; it means that if any graph containing this configuration cannot be 4-colored, then there’s a smaller graph that also cannot be 4-colored.
2. My second point is philosophical. The proof of 4CT is, I think, not quite as bas as it is being made out to be – and in fact I think it’s not as controversial today as it is sometimes described. I’ll separate two common criticisms of the proof:
* The proof is suspect of being false, say because it cannot be perceived in full by a person. In fact, it’s no more “suspect” than most convoluted, long proofs that appear in math journals. Sure, the program could be buggy, but this particular program (and many variants) was by now run so many times that a consistent misleading bug is a lot less likely than a subtle error in a human-generated proof that was only read by a handful of experts. A lot of errors and incomplete arguments can be found in papers, and many human proofs are so long that nobody can perceive them either.
* The proof is not “revealing” enough – it leaves it a mystery *why* the theorem is true. That may be true, but it doesn’t really have anything to do with the number of configurations. Suppose someone were to find a set of 37 irreducible configurations; those can be checked by hand, with some labor. Computers are no longer needed, but is the proof now “revealing”? I hardly think so.
In fact, the miracle of the proof is really the fact that a finite set of reducible, unavoidable configurations exists at all. Heesch originally came up with a heuristic argument that such a set should exist, and understanding this heuristic intuitively is all one really needs to “see” the 4CT. The sad fact that an actual such set turns out to be somewhat large is really besides the point; the big conceptual step is going down from infinitely many graphs to N configurations, not from 1476 configurations to 37. If someone were to achieve the latter it would be awesome, but it won’t change the fact that the heart of the matter lies in the “finitization”.
Just my 2c.
– A. A.
Actually the reason why this proof is disliked by most “pure” mathematicians is very, very simple.
The mathematical statement “a map can be coloured with at most four colours” is so simple it is almost banal the proof is so complex it is almost impossible for most people to understand. The whole situation is just plain ugly! And that’s all there is to it. A simple claim should have a simple elegant proof!
Alon’s description of 4CT reminds me of string theory. Its “finitization” of the a priori (and in regular QFT’s realized) infinite number of vacua lead to the large landscape.
And still people complain. 😛
Thony: I actually don’t think people dislike the proof because it’s so complex. Pure mathematicians are very used to the fact that simple claims often have proofs that are very, very far from simple – and if I do speak for myself here, I don’t “dislike” this at all. That’s part of the attraction, actually.
In fact, the proof of 4CT is not nearly as complex as many other proofs of relatively simple-to-state theorems. Wiles’ proof of FLT, or Faltings’ proof of Mordell’s conjecture, are many orders of magnitude more difficult than the proof of 4CT. Maybe people dislike those proofs (I don’t think so, really), but nobody really expects those simple statements to have simple proofs.
What could be more beautiful than harnessing complex analysis to prove that every arithmetic progression contains infinitely many primes, unless its members are all divisible by some prime p? This is simple to state, totally not simple to prove, but extremely elegant.
Torbjörn, does the “landscape” actually give us a specific, finite number of states to work with? I seem to remember a cross-blog argument a few months ago about exactly what the number of points in the landscape was, which appeared to be 10^500, 10^1000, or unlimited, depending on who was doing the reasoning. I never quite figured out what the result of that argument was but one consistent thing that did seem to come out of it is that “10^500” was basically just somebody’s idiomatic way of expressing of “a really large number” or “an exponent of an exponent” that had become institutionalized through repetition. This seems a bit different from the 4CT irreducible states, where we have a very specific integer number and a proof that there are no more than that.
Coin, I am a layman here, but my understanding is that it is possible to count the number of possible “compactifications” and that the consensus is that 10^500 is a good estimate. (Or at least a convenient number to use.) But I have stumbled claims of 10^100 or an infinite number too.
Btw, AFAIU the lower estimates give environmental or anthropic principles problems to explain an unnatural cosmological constant of ~ 10^-123 in planck units, because they need a fair distribution of vacuum states down to (and possibly below) 0. So I think string physicists are interested in improving these estimates.
I agree, the number of states here has little parallel to 4CT. (Except perhaps if someone finds a method to pick out a unique and correct one.) It was mostly a jest. But not totally, as Alon I don’t see what says that simple results (assuming string theory gives a definite one eventually) has simple proofs. Finite proofs, by necessity; simple, no. 🙂
(Unfortunately this will be another long post. It has some neat trivia in it, though.)
1. Chu-Carroll’s statement “Every planar graph is also the structural equivalent to a map, where the vertices corresponding to two countries on a map are adjacent if and only if the countries share a border in the map” is false. There are topologically messy maps which require as many as 6 colors. One showed up in the American Mathematical Monthly a few years ago; the title of the article is “Four colors do not suffice.”
2. The 4CT was also proved by Robertson, Sanders, Seymour, and Thomas, with a smaller unavoidable set, a smaller set of discharging rules, and better proof techniques. They also provide a quadratic-time algorithm for 4-coloring a planar graph. (Appel and Haken only provide a quartic-time algorithm.) The new proof was verified by proof-verification software about five years ago.
(BTW, Thomas was my doctoral advisor. At the start of graduate school, I did research marginally related to the 4CT proof.)
3. Robertson, Seymour, and Thomas have also moved on to generalizations of the 4CT. They announced a proof, at Rutgers in 1998, that every 3-regular 2-connected graph can be 3-edge colored unless it contains a minor isomorphic to the Peterson graph. (Hence, as a consequence, every snark contains the Peterson graph as a minor.) Since this result is a generalization of the 4CT, it must be “harder to prove”, and indeed it is messy but uses a lot of the machinery that RSST used on the 4CT.
4. Another result about 4-colorability of planar graphs is the (former) conjecture that any triangulation which has only one 4-coloring (shuffling colors doesn’t count as a new coloring here) contains a vertex of degree 3. This was proven by Tom Fowler in the late 1990s and uses pretty much the same unavoidable set and discharging rules.
5. Before Appel and Haken, there were quite a few results of the form “If a planar graph G has at most k vertices, then G is 4-colorable”, which do not use computer proofs. The last one was proven by Mayer in 1976, with k=95.
6. Lorenz Friess proved that if you have a planar graph which is almost a triangulation (there is exactly one face which is not a triangle), then it is 4-colorable (and it has a guaranteed number of colorings). This paper has only appeared in German, and I am “working” on translating it into English.
— Christopher Heckman
Four Colors Do Not Suffice
Hud Hudson
The American Mathematical Monthly, Vol. 110, No. 5 (May, 2003), pp. 417-423
doi:10.2307/3647828
This article consists of 7 page(s).
Is there an overlooked counterexample to the celebrated “four-color conjecture”? Well, that depends on exactly how the conjecture is formulated, and unfortunately, formulations that are widely taken to be equivalent may in fact not be equivalent. This paper relates the peculiar history of Zenopia – an island country with six provinces whose boundaries apparently threaten the conjecture, and whose existence teaches us a lesson we may name “the cartographic many-color thesis.”
I like wikipedia’s summary of this, which in particular notes that the four-color theorem assumes all regions are contiguous, something which isn’t true in real maps:
To I. Cahit:
I have tried to read and understand the paper that you link to above, and as an interested layman I find it quite interesting, but a little difficult to follow, because of imperfections in the use of the English language. It would greatly help my understanding if you could improve the paper in this respect. For example, you could rely more on mathematical formulas instead of running text.
The illustrations on the other hand are very helpful. In fact I’ve spent most of my time so far by looking at figure 7 and figuring out why your coloring algorithm succeeds on it. Your definitions and theorems on the preceding pages presumably prove that this is the case but I don’t understand them yet.
Re: #17
Reinier Post, are you by any wild stretch of probability related to the great logician Emil Post?
I am NOT related to that Post. I keep telling you that. So stop sending me those unpaid bills. [joke]
Nor am I related to the E. J Post of “Formal structure of electromagnetics: General covariance and electromagnetics” and “Can microphysical structure be probed by period integrals?”
Phys. Rev. D 25, 3223 – 3229 (1982)
[Issue 12-13; June 1982]
[E. J. Post
8634-3 Pershing Drive, Playa del Rey, California 90291]
But due to the co-California addresses, we HAVE gotten mail intended for each other.
To: Reinier Post
“I have tried to read and understand the paper that you link to above, and as an interested layman I find it quite interesting, but a little difficult to follow, because of imperfections in the use of the English language. It would greatly help my understanding if you could improve the paper in this respect. For example, you could rely more on mathematical formulas instead of running text.
The illustrations on the other hand are very helpful. In fact I’ve spent most of my time so far by looking at figure 7 and figuring out why your coloring algorithm succeeds on it. Your definitions and theorems on the preceding pages presumably prove that this is the case but I don’t understand them yet.”
Yes I know that my English is not perfect and I also know that the style of my paper needs more symbolic or mathematical statements. In the final version (hopefully appear soon)
1. I have corrected some minor errors in my algorithm e.g., the use of single Kempe-switch in case of the sailing boat subgraph. I also add as an alternative to the spiral-segment coloring the three-plus-one spiral chain coloring algorithm.
2. I have given exact justification of the spiral chain coloring algorithm and three-plus-one spiral chain coloring.
3. Some parts from the introduction and figures will be deleted.
I am not in hurry in re-writing this version because of the character of the four color problem. I mean easy to state but diffuclt to prove.
In order to get an idea about the my final version of my spiral chain proof of the 4CT please look at my web-site at the flickr.com
http://www.flickr.com/photos/49058045@N00/
I. Cahit
Jonathan: no well-known relatives here. It may interest you that Post, like other Dutch surnames such as Bot, Schelvis, Wijting, and Haring, is a species of fish.
I. Cahit: it would be instructive to have an interactive graph generator and colourizer, to see your principles in action. Perhaps I can take that up as a toy project one day.
arXiv:0707.3373 [ps, pdf, other]
Title: How Much Work Does It Take To Straighten a Plane Graph Out?
Authors: Mihyun Kang, Mathias Schacht, Oleg Verbitsky
Comments: 3 pages
Subjects: Combinatorics (math.CO)
We prove that if one wants to make a plane graph drawing straight-line then in the worst case one has to move almost all vertices.