A Proof No One Could Read

The four-color problem is easy to state: can every flat map be colored with four colors so that no two neighboring regions share one? For a century mathematicians believed the answer was yes and could not prove it. In 1976, Kenneth Appel and Wolfgang Haken announced a proof of an unsettling new kind. They had reduced it to nearly two thousand troublesome configurations and set a computer to check each one, over a thousand hours of machine time. No human had read the whole proof, and no human ever would.

Mathematicians accepted the theorem and argued about the proof. By long tradition, a proof's authority comes from surveyability: a competent reader can follow every step and be convinced by reason alone. Here a crucial stretch of reasoning lived inside a machine, and one philosopher argued the theorem was now known the way experimental results are: by trusting apparatus.

The sequel reversed the complaint. In 2005 the proof was rebuilt inside a proof assistant, a program whose small logical kernel verifies every inference of every step, including the parts referees usually skim. The unread stretch is now the most thoroughly checked part of the theorem. The lasting question is no longer whether a machine's proof deserves our confidence, but whether an unaided reader's ever did.