The Four Color Theorem — When a Computer Carried Part of a Proof

The four color theorem states that any map in the plane can be coloured with four colours so that regions sharing a border never get the same colour. Posed in 1852 and unsolved for more than 120 years, it was proved in 1976 by Kenneth Appel and Wolfgang Haken of the University of Illinois. MacTutor, the history-of-mathematics archive at the University of St Andrews, records that on 21 June 1976 the two announced that they had proved the four colour conjecture with the aid of a computer.

The proof matters less for its conclusion than for its shape. Its core was a computer check of nearly 1,500 "configurations", one at a time, and no human could verify the whole thing by hand. Whether a proof that nobody can read through deserves the name became a major controversy, and the question has carried over, half a century later, into the era in which AI systems write proofs.

An 1852 question and a proof that failed

According to MacTutor, the question goes back to Francis Guthrie in 1852. His brother Frederick put it to Augustus De Morgan, who wrote to William Rowan Hamilton the same day, 23 October 1852. De Morgan's letter opened: "A student of mine asked me today to give him a reason for a fact which I did not know was a fact."

Kempe's proof stood for eleven years. MacTutor quotes Heawood's 1890 paper describing its aim as "rather destructive than constructive", since it set out to show a defect in what was then widely accepted. The four colour problem became known as a problem whose plausible proofs fall apart later.

Appel and Haken: unavoidable sets and reducibility

The proof combines two ideas that go back to Kempe. Build a set of configurations that must appear in every map (an unavoidable set), then show that every configuration in the set can be reduced to the colouring of a smaller map (that it is reducible). If both hold, no counterexample can exist.

The difficulty was the size of the set. The 1976 announcement, as quoted by MacTutor, says nearly fifteen hundred configurations were required, most of them not previously published, and that 1,200 hours of computer time were used for the reductions.

A University of Illinois profile says Haken became interested in the problem after hearing a lecture by Heinrich Heesch in 1949, worked on it in the 1960s, and concluded that a breakthrough would need a powerful computer. That led him to Appel, a colleague who was an expert in programming. Haken later said of their share: "We did the last 20 percent." He counted the pair as the fifth generation of people to work on the problem.

The Illinois mathematics department honoured the result by adding the words "Four Colors Suffice" to its postal meter. The image on this page is one of those strips, dated 30 September 1976.

Can a computer be part of a proof?

In the same profile Haken recalled that the announcement was greeted by some with enthusiasm and by others with scorn. While a documentary was being filmed at a New York college in 1981, one mathematics professor would not let his students talk to Haken or Appel at all. Haken remembered the objection put to him: "One person told me, quite correctly, 'How can a computer be part of a mathematical proof?'" and added, "A computer is a physical apparatus."

From philosophy, Thomas Tymoczko argued in the Journal of Philosophy in 1979 that a proof should be surveyable by the human mathematical community, and that the Appel–Haken proof substituted experiment for deduction. The debate moved beyond one theorem to the question of what a proof is.

Robin Thomas of Georgia Tech lists two concerns that remained. Part of the Appel–Haken proof uses a computer and cannot be verified by hand, and even the part that is supposedly hand-checkable is extraordinarily complicated and tedious.

A second proof and a machine-checked one

The second proof of 1997 answered those concerns. Neil Robertson, Daniel Sanders, Paul Seymour and Robin Thomas rebuilt the argument with 633 configurations and 32 discharging rules, against more than 300 in Appel and Haken's version, and published it in the Journal of Combinatorial Theory, Series B. A computer was still needed, but on a far smaller scale.

In 2005 Georges Gonthier and Benjamin Werner then verified the entire proof formally in the Coq proof assistant. Instead of trusting a program's output, another program checks every step against the rules of logic. The same approach was later used to settle the Kepler conjecture through the Flyspeck project (2014), a proof its referees could not fully certify.

What changed, and for whom

What changed was the working assumptions of mathematicians. MacTutor sums up that, despite initial worries, independent verification soon convinced everyone that the theorem had been proved. The price was a new set of questions about refereeing, about how checking is divided between people and machines, and about where certainty actually lives.

Those questions returned in a different form once AI began solving International Mathematical Olympiad problems in 2024. AI proofs checked in the Lean proof assistant are descendants of the Coq verification of the four colour theorem. And the question of what to do with proofs no human has read through became central again in the debate over Erdős problems and AI in 2026. The longer story of computers and mathematics is on the AI and mathematics timeline.