1. The Answer Is Four Colors, and Three Are Not Enough
The rule is simple: two regions that share a stretch of border must get different colors. Regions that touch only at a single point do not count as neighbors.[1]
It is easy to draw a map that needs four colors. Cut a disk into three wedges, A, B and C, and surround it with a ring, D. Every pair of those four regions shares a border, so all four need different colors.
So four is the minimum for some maps. The surprise is that you never need five. Any map drawn on a flat sheet, or on a sphere, can be colored with four colors. This is the four color theorem, and today mathematicians accept it as proved.[1][2]
One catch: this is about maps where each region is a single connected piece. If a country has islands or exclaves that must share its color, four colors can fail. Gonthier points out that regions made of several separate pieces can need more, and that the number can grow without bound as the pieces multiply.[3]
2. Why Trying Lots of Maps Is Not a Proof
The question began in 1852. A student, Francis Guthrie, was coloring a map of the counties of England and noticed that four colors seemed to be enough. He passed the question to his brother Frederick, who asked his own teacher, the mathematician Augustus De Morgan.[1] De Morgan wrote to a friend that a student had asked him for a reason for a fact "which I did not know was a fact, and do not yet."[4]
Coloring a thousand maps would not settle it. Maybe the next map is the one that breaks the pattern. To prove the claim for every possible map, you need an argument that covers all of them at once, and for a very long time nobody could find one.
3. Kempe's "Proof" Looked Right for 11 Years Before Heawood Found the Hole
In 1879, Alfred Kempe published a proof, and it was widely praised. In 1890, Percy Heawood showed it had an error. Another proof, by Peter Guthrie Tait in 1880, was refuted in 1891 by Julius Petersen. Each had stood for about 11 years.[1] Heawood described his own paper as "rather destructive than constructive," because it showed a defect in the proof everyone had accepted.[4]
Heawood did not only break things. Using Kempe's method, he proved that five colors always suffice, which is called the five color theorem.[1] The gap between four and five is just one color, but closing it took until 1976. This history is also why mathematicians stayed nervous: this problem had a record of proofs that looked right and were not.[2]
4. How a Computer Helped Appel and Haken Prove It in 1976
On June 21, 1976, Kenneth Appel and Wolfgang Haken of the University of Illinois announced a proof.[1] The idea is a proof by contradiction. Suppose some map cannot be colored with four colors, and take the smallest such map. Two things then have to be shown.
- Unavoidable: every map must contain at least one shape from a certain list of shapes.
- Reducible: if a map contains one of those shapes, you can shrink it into a smaller map, and a four-coloring of the smaller map can be turned into a four-coloring of the original.
If both are true, the smallest bad map cannot exist, because it would contain a shape that lets you build a smaller bad map. The proof therefore needed a list of shapes that was truly unavoidable, with every shape on it checked for reducibility. According to Wikipedia, Appel and Haken reduced the endless variety of maps to 1,834 configurations (later trimmed to 1,482), and a computer spent more than a thousand hours checking them. The part showing the list was unavoidable filled over 400 pages and was checked by hand. I could not confirm these figures in a primary source.[1]
Gonthier notes that this was the first long-standing mathematical problem resolved with the help of a computer program. In his words, it involved a case analysis that could not "in any real sense" be done by hand, covering "quite literally, a billion cases."[3]
5. Can a Proof That Nobody Can Read All the Way Through Be Trusted?
Many mathematicians were uneasy. Part of the criticism was about style: the statement is short and elegant, so people hoped for a short, elegant explanation of why it is true. A proof carried by a pile of computer output does not explain much. Another part was more practical. Programs are error-prone, and it is hard to be sure a program really checks what the theorem says. On top of that, the hand-checked case analysis was large, about 10,000 cases.[3]
The team that later redid the proof gave two reasons for doubt: part of the original proof relied on computer checks that were too extensive to repeat by hand, and even the part meant to be checked by hand was extraordinarily complicated, with no complete independent check that they knew of.[2] They called the second reason the more disturbing one, since the problem already had a history of incorrect proofs.[2]
So the doubt was reasonable, not stubborn. The question was how to remove it.
6. How Later Teams Re-Checked the Proof With Fewer Cases and a Proof Checker
In 1993, Neil Robertson, Daniel Sanders, Paul Seymour and Robin Thomas decided to convince themselves the theorem was true. They tried to read the original proof, soon gave up, and wrote their own along similar lines. It took about a year. Their list has 633 configurations instead of a much larger set, they needed 32 "discharging rules" where Appel and Haken used more than 300, and they wrote the unavoidability part in a formal style that a computer can check in a few minutes.[2] Their paper was revised on January 16, 1997.
Georges Gonthier later formalized the whole argument. He wrote the whole argument, both the mathematics and the computing, as a script for the proof assistant Coq, which checked every logical step mechanically.[3] Wikipedia dates this to 2005.[1] A skeptic can still ask whether the computer, the operating system and Coq itself are right. But Gonthier argues that these are general-purpose tools used and tested on countless other jobs, and that Coq can produce a detailed record of its logical steps that could in principle be checked independently.[3]
Today most mathematicians accept the theorem. What nobody has found is a short proof that a person can read and understand. Whether you must be able to understand a proof for it to count is a question the four color theorem pushed into the open, and people still disagree about it.[1]
7. Ways to Investigate the Four Color Theorem Yourself
Try this on paper. Draw a map with at least ten regions and color it with as few colors as you can. Then try to build a map that forces you to use four. Did you ever feel tempted to use a fifth color? If you did, try changing the colors and see whether you can avoid it.
Then read the primary sources. The opening pages of the Robertson, Sanders, Seymour and Thomas paper and Gonthier's report both explain, in plain language, why people doubted the 1976 proof. Ask yourself where you would draw the line between "I checked it myself" and "I trust the people and tools that checked it."