# Every planar graph can be colored with 4 colors max

Ok, that's a theorem. As it says in this question.

I just cannot understand how mathematics can prove such a thing; what does exactly this theorem say? How to prove it mathematically?

Thanks!

-
You could read the proof of the 6 color theorem, which is immensely simpler, to get an idea of how one does such things. – Mariano Suárez-Alvarez Nov 9 '10 at 16:03
(Next, you could move to the 5 color theorem, which is a bit more elaborate. You can find these results using google quite easily) – Mariano Suárez-Alvarez Nov 9 '10 at 16:04
I will! Thanks! – Diego Nov 9 '10 at 16:21
Since the proof of the four colour theorem is not yet very human-readable, you may also consider reading the nice account in press.princeton.edu/titles/7495.html – Willie Wong Nov 9 '10 at 18:05
You might try this on-line tutorial about coloring problems in general as a way to see how theory about coloring graphs develops: primes.utm.edu/cgi-bin/caldwell/tutor/graph/color – Joseph Malkevitch Nov 9 '10 at 18:18

The first proof was due to Appel and Haken in 1977. However, as pointed out by Willie Wong, it is not really readable. Very roughly, it first uses a classification of almost 1500 "unavoidable configurations" of the triangulation of a plane. Next, using computers, it is shown that every of these configuration "leads" to a 4-coloration.

Appel and Haken published an algorithmic approach to this problem in K. Appel and W. Haken, Every Planar Map is Four-Colorable, American Mathematical Society 1989.

In 1997, another proof was published but still use the computer in a similar way. This was due to N. Robertson, D. Sanders, P.D. Seymour and R. Thomas.

To answer to your question How can math prove such a thing?, we see that computer plays a fundamental role in this particuliar problem. In fact, computer science plays a very fundamental part in today's research in finite structures. For instance, the Classification of the Finite Simple Groups is another very famous example. Computers were needed in several parts of the proof as they still are.

Now it does not reduce these results to "uninteresting" simply because computers are needed to prove them. To the contrary, the efforts needed for the conception and the implementation of such algorithms is in itself a very remarkable work.

In conclusion, mathematics can prove such things through algorithmic approaches and clever implementations in computers.

As a final remark, note also the following result due to Grötzsch, 1959:

Every planar graph not containing a triangle is 3-colorable.

-
Let's not forget Gonthier's version! – Yuval Filmus May 19 '11 at 4:19