The Proof That Needed a Machine

On 23 October 1852, a student named Francis Guthrie was colouring a map of the counties of England. Four colours seemed to be enough. He asked his brother Frederick whether that was always true, and Frederick asked his professor, Augustus De Morgan. De Morgan did not know. He wrote to William Rowan Hamilton in Dublin, and a small question began its long career as a mathematical embarrassment.

The question was almost offensively easy to state: can every map be coloured with four colours so that neighbouring countries have different colours? Countries meeting only at a point do not count as neighbours. Take a pencil and try it on an ordinary map. The puzzle feels like a matter of patience, not the sort of thing that should occupy mathematicians for more than a fortnight.

It occupied them for 124 years. When the answer finally arrived, it came with a surprise that was almost as troubling as the answer itself: a computer had done part of the proving.

The proof that looked finished

In 1879, Alfred Kempe published what appeared to be a proof. It contained a useful idea. If a colouring gets stuck around a region, one can sometimes swap two colours along a connected chain of countries and free a colour for the region in trouble. These became known as Kempe chains.

The argument worked for regions with three or four sides. Kempe believed it also worked for five-sided regions, where the difficulty lies in the possibility that two chains interfere with each other. They can be rearranged in one order, but the first rearrangement may destroy the conditions needed for the second. The proof had quietly assumed that two moves could be made independently when they could not.

Percy Heawood found the gap in 1890. He also proved something weaker but valuable: five colours always suffice. The four-colour problem went back into the cupboard, still visible through the glass. Other attempts came and went. Peter Guthrie Tait produced another false proof in 1880; later work showed that its own crucial step failed too.

This history mattered. A conjecture with a simple statement had already defeated confident people, and one of its most celebrated proofs had survived for eleven years before anyone noticed the crack. The eventual solution would not be allowed to rest on elegance alone.

A map reduced to a finite hunt

The breakthrough depended on replacing “every possible map” with a finite collection of local patterns.

The strategy, developed especially by the German mathematician Heinrich Heesch, had two parts. First came unavoidability: show that every hypothetical map requiring five colours must contain at least one pattern from a chosen list. Second came reducibility: show that none of those patterns could occur in the smallest possible counterexample, because the pattern could be replaced by something smaller. If every counterexample had to contain a thing that no smallest counterexample could contain, there was no counterexample.

The language is forbidding, but the shape of the argument is familiar. Imagine proving that every locked room must contain a key, then proving that a locked room cannot contain a key. The unusual part was the size of the key ring.

In the early 1970s, Kenneth Appel and Wolfgang Haken at the University of Illinois decided to make the search practical with computers. They did not ask a machine to invent the theorem from nothing. They designed the mathematical rules, the list-making procedure and the tests. The computer performed the vast enumeration that people could specify but could not sensibly carry out by hand.

Their 1976 announcement reported an unavoidable set of fewer than 2,000 configurations. The later technical papers used a list ultimately reduced to 1,482 configurations. Each had to pass a reducibility check. The original work required roughly 1,200 hours of computer time, a figure that made the proof both possible and difficult to read as a proof.

The machine had not replaced the mathematicians. It had become a very fast, very literal member of the team, one that could not be persuaded by a beautiful diagram and could not explain its entire afternoon.

The problem was no longer only whether the theorem was true. It was whether a calculation too large for a person to inspect could count as proof.

The scandal of being correct

Mathematicians were not simply hostile to computers. They had used calculation for years. The discomfort was more specific: a traditional proof offers a chain of steps that, at least in principle, a reader can follow. Appel and Haken’s proof included hundreds of pages of diagrams and a computer-dependent portion that could not be checked line by line with pencil and paper in any reasonable lifetime.

There was an additional reason for caution. The four-colour problem already had a history of plausible errors. The original proof was corrected after publication, and its human-readable parts were long and intricate. Running a program twice and getting the same answer is not the same as proving that the program is right. A bug can be perfectly consistent.

The result was accepted, but not with the smoothness that usually attends a famous theorem. In 1994, Neil Robertson, Daniel Sanders, Paul Seymour and Robin Thomas produced a new proof using the same broad architecture. They reduced the unavoidable set to 633 configurations and made the argument easier to check. It still required a computer for some verification. The machine had not been evicted; it had been given a smaller desk and better paperwork.

That distinction is important. The second proof did not restore an imaginary age in which mathematics was untouched by computation. It showed instead that the argument could be reorganised so that more of its structure was exposed and less of its trust had to be placed in one enormous calculation.

When the proof became a program

The final turn came from formal proof. Georges Gonthier and collaborators encoded the mathematics in the Coq proof assistant, completing the formalization in 2005 and describing it in 2008. This was not merely a new program that repeated the old calculation. The definitions, logical steps and computational checks were written in a form that Coq could verify according to its underlying rules.

The difference is subtle but decisive. In the Appel–Haken style, a paper says that a program has checked a finite list of cases. In a formal proof, the program is part of a system that checks the statements about those cases and the logical connections between them. The computer is not being asked only, “Did this run return true?” It is being asked to reject any step that does not fit the formal rules.

That does not create certainty from nowhere. The formal proof still depends on hardware, software and the correctness of the proof assistant itself. But the dependence is made explicit and general. A reader need not trust a bespoke program because its authors say it worked; the checker can produce a proof object whose logical structure is available for independent scrutiny.

The map on Guthrie’s desk was never really about maps. It was about the boundary between seeing and knowing. A person can understand the theorem’s statement in seconds, yet the shortest route to its proof passes through thousands of local configurations, failed arguments, algorithms and machines. The result forced mathematics to admit that a proof can be too large for a human mind to survey in one sweep without being meaningless.

Four colours suffice. That sentence is now secure, but its history leaves a more consequential mark: sometimes the honest way to preserve a proof’s human idea is to let a machine carry the parts no human can hold, then build a second machine whose job is to distrust the first.