Better algorithms. More possibilities

The four color theorem

Four colors suffice

• The proof that needed a computer

  Draw a map as intricate as you like. Four colors will always be enough to ensure that no two neighboring regions share the same color.

  First posed in 1852, the problem resisted mathematicians for more than a century, until Kenneth Appel and Wolfgang Haken proved the theorem in 1976 with the help of a computer.

  To this day, no proof without a computer is known: every later proof still has a computer check hundreds of cases.

• That spirit of discovery is at the heart of 4colors

  The four color theorem was the first major theorem proved with the help of a computer.

  We follow the same path: mathematical insight, then automated algorithm discovery that tries far more ideas than people can by hand, and rigorous benchmarking before a discovery becomes a carefully tested algorithm.

• Watch the algorithm at work

  The solver uses a classic graph coloring algorithm, DSatur, which tackles the most constrained regions first. It colors the map in your browser, in real time, then replays the solution so you can follow its decisions.

  Hover over a region, or tap it, to discover its neighbors.