The Four-Color Problem
map

The story goes, the Four Color Problem dates back to 1852 when Francis Guthrie, while trying to color the map of counties of England noticed that four colors sufficed. He asked his brother Frederick if it was true that any map can be colored using four colors in such a way that adjacent regions (i.e. those sharing a common boundary segment, not just a point) receive different colors.

For a very long period, some of the best mathematicians struggled to prove that, yes, four colors are indeed sufficient. Many people thought to have delivered a valid proof, only to discover flaws in their thinking subsequently.

Finally, the year 1976 saw a complete solution to the Four Colour Problem. The proof was achieved by Appel and Haken, using 1200 hours of computer time to work through the details of the final proof.

The Four Colour Theorem was the first major theorem to be proved using a computer, having a proof that could not be verified directly by other mathematicians. Despite some worries about this initially, independent verification soon convinced everyone that the Four Colour Theorem had finally been proved.