The AI Journal

In June 1976, Kenneth Appel and Wolfgang Haken announced that every map drawn on a plane could be coloured with four colours so that no two adjoining regions shared one, closing a problem posed by Francis Guthrie in 1852. Their proof reduced the infinite class of possible maps to an unavoidable set of 1,936 configurations, using 487 discharging rules to show that at least one of them had to appear in any hypothetical smallest counterexample; showing each configuration reducible took roughly 1,200 hours of computer time, a case analysis too large for any mathematician to complete, or even check, unaided. The announcement produced not celebration but an argument that ran for a decade and, in modified form, has never fully ended: whether what Appel and Haken produced counted as a mathematical proof at all.

That argument is now remembered, when it is remembered, as a dispute the mathematical community eventually won on the merits. The University of Illinois postmarked its outgoing mail “Four colors suffice,” rivals hunted for an error and found one — Ulrich Schmidt, an engineering student at Aachen, discovered a fault in the discharging procedure in 1981 that took Haken two weeks to repair — and Appel and Haken answered the resulting rumours in 1986 with a paper bluntly titled “The Four Color Proof Suffices.” Neil Robertson, Daniel Sanders, Paul Seymour and Robin Thomas produced an independent, smaller proof in 1997, still computer-assisted but cut to 633 configurations, that corroborated the result without depending on the original code. And in 2004, Georges Gonthier completed a full formalisation of the whole argument in the Coq proof assistant, checked not by running a discharging program once but by a kernel that verifies, step by mechanical step, that every inference in a several-thousand-line proof term follows from the axioms of a formal logic. On the usual telling, this sequence is a reliability story with a happy ending: an unverifiable computation was gradually replaced by a fully verifiable one, and the doubt that Appel and Haken’s program first provoked was answered by better engineering.

It was answered. It was also not the doubt that gave the controversy its philosophical importance. Thomas Tymoczko’s 1979 paper on the case, published two years after the Illinois Journal of Mathematics printed the original proof, did not argue that Appel and Haken’s program might contain a bug — a possibility he barely raises — but that even a bug-free version of their proof would fail to be a mathematical proof in the sense the word had always carried. Tymoczko’s claim rested on a feature he took to be constitutive of proof rather than incidental to it: a proof is something a suitably trained mathematician can survey, step by step, and thereby come to know the theorem is true purely by following the argument. What made the four-colour proof different in kind, on his account, was not its length but that no mathematician surveyed the case analysis at all; a machine executed it, and the community’s warrant for believing the conclusion rested on trusting a computation nobody had followed, which he took to be closer to trusting an experimental result than to possessing a proof. Reliability and surveyability are different properties. A discharging program can be checked for bugs, rerun on independent hardware, and cross-validated by an unrelated proof, as Robertson and his co-authors eventually did — all of which increases confidence that the conclusion is true without giving anyone a case analysis they can actually read through.

Gonthier’s formalisation is the most sophisticated answer available to the reliability worry, and it is worth being precise about why. Coq’s trusted computing base — the kernel code whose correctness the whole edifice depends on — is small enough that it has itself been read and independently reimplemented by other research groups; everything checked against it, including a proof term of many thousand lines encoding the discharging and reducibility arguments, is verified by a fixed, auditable procedure rather than by trusting whichever program a research group happened to write. This is a genuine advance over 1976, when the correctness of the result rested on trusting one purpose-built program that nobody outside its authors’ research group could easily inspect, and it explains why formalisation projects have become the standard reply mathematicians now reach for when a computer-assisted result draws suspicion. But none of this restores what Tymoczko said proof required. A mathematician who accepts the four-colour theorem on the strength of Gonthier’s certificate is still trusting a computation nobody surveys; formalisation replaced an unaudited program with an audited one, not an unsurveyed argument with a surveyed one. If anything the gap widened, since the proof term Coq checks is longer, more mechanical and further from ordinary mathematical prose than Appel and Haken’s already unreadable case tables were. The 2008 result closes the sociological controversy — did this particular team’s code have an error nobody caught? — by a route that leaves the 1979 philosophical one exactly where it was.

The strongest reply available to Tymoczko’s position, and to the argument built on it here, is that surveyability was never a coherent requirement for proof in the first place, and demanding it proves too much. Mathematicians already accept results that depend on computations they have not personally checked: numerical routines inside a computer algebra system, floating-point calculations in other large computer-assisted proofs, even long multiplication carried out by hand far past the point a reader troubles to re-verify each digit. If trust in an unread computation is disqualifying, most of contemporary mathematics that leans on a computer algebra package falls with the four-colour theorem, which suggests the objection proves too much to be doing real philosophical work. This is a fair point, and it should narrow the claim rather than defeat it. What distinguished Appel and Haken’s case analysis, and distinguishes Gonthier’s proof term after it, is not merely that a computer did the work but that the work was, from the outset, of a kind no human could have carried out by hand even given unlimited time and patience, unlike a long multiplication or a routine matrix computation that a person could in principle grind through as an extension of ordinary calculation, or a compiler’s output, which a programmer can in principle trace instruction by instruction even when nobody does. The 1,936 configurations were never of that kind; nobody designed them to be checkable in the way a long calculation is checkable, only to be correct, and Gonthier’s kernel inherits that property rather than removing it. Formalisation answers the question of whether that unsurveyable computation was executed correctly. It does not, and by its own mechanical nature cannot, turn the computation into one a mathematician could survey. The controversy the four-colour theorem opened in 1976 was about whether that distinction matters to what counts as proof; verifying the arithmetic more rigorously was never going to be the kind of answer that question required, and the fact that it is now the best answer available says more about the limits of the reply than about the strength of the objection it was meant to settle.