On this page
Draw any map you like, as long as each country is one connected piece. You will never need more than four colours to keep neighbouring countries different. Francis Guthrie noticed this in 1852 while colouring a map of the counties of England (Robin Thomas, Georgia Tech). Proving it took until 1976, and Kenneth Appel and Wolfgang Haken needed a computer to do it.
What did Appel and Haken prove in 1976?
The four colour theorem says that any map can be coloured with four colours so that adjacent regions get different colours (Thomas). Adjacent means sharing a stretch of border, not just a single point.
The question soon reached the London mathematician Augustus De Morgan, who wrote to William Rowan Hamilton: "A student of mine asked me today to give him a reason for a fact which I did not know was a fact - and do not yet" (MacTutor History of Mathematics). In 1879 Alfred Kempe announced a proof, and in 1890 Percy Heawood showed it had a flaw (same source).
Appel and Haken announced their proof in a two-page note, "Every planar map is four colorable", in the Bulletin of the American Mathematical Society in 1976. The full argument appeared in 1977 in the Illinois Journal of Mathematics in two parts, Part I: Discharging and Part II: Reducibility, the second written with John Koch (Illinois Distributed Museum).
How did a computer prove the four colour theorem?
The proof works like a trap.
Imagine the smallest map that needs five colours, the minimal counterexample.
Find a list of small patterns of regions, called configurations, such that every map contains at least one. This is an unavoidable set, built with a counting method called discharging that Heinrich Heesch introduced in 1969 (MacTutor).
Show each configuration is reducible: it cannot appear in a minimal counterexample.
The minimal counterexample must then contain a pattern it cannot contain, so it does not exist.
Step 3 is where the computer came in. According to MacTutor, Appel and Haken built an unavoidable set of around 1,500 configurations and used 1,200 hours of computer time to work through the details. MacTutor calls it "the first major theorem to be proved using a computer".
Why did mathematicians doubt a proof by computer?
Robin Thomas, who later helped reprove the theorem, writes that part of the Appel-Haken proof "cannot be verified by hand, and even the part that is supposedly hand-checkable is extraordinarily complicated and tedious" (Thomas).
The computer "brought considerable initial criticism", which later faded (Illinois Distributed Museum). The same page notes that the Urbana post office made a postmark that read "four colors suffice".
Two later steps settled the doubts:
In 1997, Neil Robertson, Daniel Sanders, Paul Seymour and Robin Thomas published a new proof in the Journal of Combinatorial Theory, Series B. It uses 633 configurations instead of 1,476, and 32 discharging rules instead of more than 300, and its computer part can be verified in about 20 minutes (Thomas).
In December 2004, Georges Gonthier of Microsoft Research, working with Benjamin Werner of INRIA, announced a check of every step of that proof in the proof assistant Coq (Wolfram MathWorld).
Try it: why are three colours not enough?
The theorem says four is always enough. This short exercise, the map in the picture above, shows why four is sometimes needed.
Draw one country in the middle, ringed by five countries that each touch it and their two ring neighbours.
Colour the ring A, B, A, B. The fifth touches an A and a B, so it needs C. An odd ring always forces a third colour.
The middle country touches A, B and C. It needs D.
Add an outer country touching the ring but not the middle. It can reuse D.
With a ring of four, three colours are enough, because an even ring needs only two. For a real map, try our walkthrough on colouring the map of India with four colours.
What can a student learn from this proof?
Appel and Haken split one huge question into a finite list of checkable cases, then made sure the list left nothing out. You make the same move in a board exam proof when you split by cases (n even, n odd) and check each one.
Map colouring belongs to graph theory, where regions become dots and shared borders become lines. For an earlier chapter, read about Euler and the Seven Bridges of Königsberg. For when to trust a machine's maths, see computer algebra or AI chatbot for maths: which to trust?
If words like graph or planar are new, the Fermi Concept Library gives each concept in mathematics its own lesson. To practise proofs by cases, the Fermi Problem Library has a step-by-step solver that explains the reasoning rather than printing an answer.
Start with the five-country ring tonight.
