Four colours: a proof the machine checked
In July 1976 Kenneth Appel and Wolfgang Haken of the University of Illinois submitted a proof that every planar map can be coloured with four colours. It reduced the problem to a finite set of configurations, each of which had to be checked for reducibility; the authors' programs did the checking on IBM computers.
Why it matters
A problem whose first published attempted proof, the paper says, was Kempe's in 1879 was closed by a proof whose decisive part no person can check by hand, only repeat as a computation. Whether to trust a proof carried out by a machine became a practical question for mathematics.
Part I sets out a discharging procedure showing that every planar triangulation contains at least one configuration from the set; Part II, with John Koch, proves those configurations reducible. According to a footnote in Part I, when the paper was submitted in July 1976 the set was announced as 1,936 configurations; after about a hundred redundancies were removed the papers present 1,834, and the microfiche supplement shows that 1,482 suffice. Every configuration of ring size eleven or more but one was checked by the authors' programs, written in assembler, on an IBM 360-75 at Urbana, an IBM 370-158 at Chicago Circle and a 370-168 of the university's administrative data processing unit. A single fourteen-ring reduction took about 25 minutes on the 370-158 or 6 minutes on the 370-168. What the record does not claim: the widely repeated 1,200 hours of computer time; neither part of the paper gives that figure.