The First Computer Proof of Math Problem

In 1852, a student named Frederick Guthrie posed a question to his professor after watching his brother paint a British map. The question was whether it was possible to color a map with different regions using only four colors without having any adjacent regions share the same color. His professor was puzzled by this question, and it marked the beginning of a century-long pursuit to prove this was true for any map.

While multiple mathematicians took on the problem and could not find any map that required more than four colors, they also couldn't find a mathematical way to prove it. This problem could be approached mathematically with the help of graph theory by converting the map to a planar graph. The challenge, however, was that there were 1,932 possible variations of planar maps, making it an enormous task to prove by hand.

This is why the problem remained without proof until 1976 when mathematicians Kenneth Appel and Wolfgang Haken finally cracked the case—with a catch. They used a computer to analyze over 1,900 different configurations, showing that four colors were indeed sufficient. It was the first significant theorem proved using a computer, igniting debates in the mathematical community about the role of computers in proving theorems.

The program required hundreds of hours of computer time, which meant that the steps of the proof, if written down, could not have been read, let alone recognized as self-evident, by a human being in many lifetimes. This proof exemplifies how computers have gradually expanded our capabilities and pushed new frontiers, even in mathematics.

Craving more? Check out the source behind this Brain Snack!