Four Color Theorem

The four color map theorem, to give it is full name, states that you never need more than four different colors to give every country on your map a color different from that of its neighbors.

Here is a map of Loveland. Even so the states of Loveland have rather crazy shapes, four colors were enough to identify them.

Loveland and Four Color Theorem

What became known as the four color theorem was proposed in 1852 by one Francis Guthrie. Since then a very large number of people have tried without success to disprove it by finding an example where it does not apply. A far smaller number of mathematicians tried equally unsucessfully to prove it by strict mathematical reasoning.

It's one of several little theorems that are easy to state and nearly obvious. In other words, nobody has the slightest doubts that the theorem is true. The problem is only that serious math can't prove it.
Another example coming up in the Hyperscript is Kepler's famous theorem about close-packing of spheres.

The four color theorem was finally proved in 1976 by Kenneth Appel and Wolfgang Haken, sort of. They used a computer to run through the large but finite numbers of possibilities. Initially their proof was not accepted by all mathematicians because it is impossible for a human to check it "by hand". Since then the proof has gained wider acceptance, although doubts remain. Maybe the software has a flaw and missed something. But even if a lot of programmers producing their own software come up with the same result, that doesn't necessarily proof anything for a true mathematician, just as the fact that the sun kept rising in the east each day for the last million / billion years does not prove that it will do so tomorrow.

With frame

6.1.3 Reading Phase Diagrams: Mixed Phases and Boundaries