Skip to content

Computer-Assisted Proof

Abstract

In 1976 two mathematicians at the University of Illinois proved a theorem that no human could check by hand, because the checking involved a computer grinding through 1,834 cases for over a thousand hours. The four-color theorem was the first major result whose proof nobody could fully read, and it split mathematics: is a proof you must trust a machine to complete still a proof? Half a century later the question has been answered pragmatically. Computers now verify proofs down to the axioms in systems like Coq and Lean, and the argument has shifted from “can we trust the machine” to “can we trust the human,” because the machine checks are the rigorous part.

The Theorem Nobody Could Read

The four-color theorem states that any map can be colored with four colors so that no two adjacent regions share a color. It was conjectured in 1852 and resisted proof for over a century, collecting famous wrong proofs along the way. On June 21, 1976, Kenneth Appel and Wolfgang Haken announced they had it. Their strategy was old: find an “unavoidable set” of configurations such that every possible map must contain at least one, and show each configuration is “reducible”, meaning a smaller map coloring can always be extended across it. The novelty was the scale. The unavoidable set had about 1,900 configurations, and proving each reducible required a computer to check colorings by brute force, over a thousand hours of machine time on the hardware of the day. The human-readable portion of the proof described the method; the actual verification lived in code and output that no person would ever read line by line.

Mathematics did not know what to do with this. A proof had always been something a competent human could in principle check and be convinced by. Here the conviction rested on trusting that a program was correct and that the hardware had not erred. Critics argued this was not a proof at all but an experiment, and that mathematical certainty had been quietly swapped for engineering confidence. The New York Times at first declined to report the result, having been burned by false four-color proofs before. Even sympathizers were uneasy: the proof was ugly, unilluminating, and unverifiable in the traditional sense, and it offered no insight into why four colors suffice.

Kepler and the 99 Percent

The pattern recurred, more sharply, with sphere packing. How should you stack cannonballs to waste the least space? Kepler conjectured in 1611 that the obvious grocer’s stack is optimal, and it too resisted proof for centuries. In August 1998 Thomas Hales announced a proof: 250 pages of mathematics plus three gigabytes of computer programs and data reducing the problem to thousands of nonlinear optimization cases. The Annals of Mathematics sent it to a panel of referees who worked on it for four years, and in 2003 reported something unprecedented in a mathematics journal: they were “99% certain” the proof was correct but could not fully verify the computer calculations and would not certify it beyond that. The journal published the human part anyway in 2005. A referee panel formally admitting it could not check a proof was the clearest statement yet that computer-assisted proof had outrun the traditional refereeing process.

Turning the Computer From Suspect to Guarantor

Hales’s response reframed the whole debate. If the worry is that you cannot trust the sprawling code, then do not trust it: write the entire proof, every step, in a formal language that a small, trusted proof-checking kernel verifies mechanically against the axioms of mathematics. He launched the Flyspeck project in 2003 to do exactly that for Kepler, and on August 10, 2014, a team completed it using the HOL Light and Isabelle proof assistants. The Kepler conjecture became a theorem checked to the axioms, its certainty no longer resting on anyone’s confidence in a 3-gigabyte program. The same happened to four colors: in 2005 Georges Gonthier formalized the entire Appel-Haken proof in the Coq proof assistant, so that trusting the result now requires trusting only Coq’s tiny kernel, not the original ad hoc software.

This inverts the 1976 anxiety. A formally verified proof is more trustworthy than a traditional one, because human referees miss errors and machines checking against axioms do not. The tools have since become a working part of mathematics. The Lean proof assistant and its mathlib library have drawn in thousands of contributors formalizing large tracts of undergraduate and research mathematics, and Fields Medalist Terence Tao has used Lean to verify his own recent results and to coordinate large collaborative proofs, treating the proof assistant as a tool for confidence and collaboration rather than a threat to it. The connection to SAT and SMT solvers runs deep: the automated engines that discharge routine logical obligations inside proof assistants are the same technology that verifies chips.

The philosophical dust has largely settled into a division of labor. Machines are better at exhaustive, error-free checking; humans are better at insight, strategy, and deciding what is worth proving. The four-color theorem still offers no satisfying human explanation of why four colors suffice, and that dissatisfaction is real. But the question of whether a computer-assisted proof counts as a proof has been answered by making the computer’s role the most rigorous part of the argument rather than the most doubtful.

📚 Sources