How long now?

I still remember the ongoing furor back then, even years after publication: was this really a proof?

Since the time of Euclid and Pythagoras, proofs of mathematical theorems had consisted of long strings of equations or geometric notations that any mathematician could read and quibble with, all marching logically, step by step, toward a conclusion. But the proof that Dr. Appel and a colleague, Wolfgang Haken, established in 1976 was of a different order.

Their conclusion, that four colors would suffice for any map, depended on 1,200 hours of computer time — the equivalent of 50 days — and 10 billion logical decisions all made automatically and out of sight by the innards of an I.B.M. computer at the University of Illinois in Urbana.

I'd love to know how long it would take to rerun this proof on some of today's machines. The answer is probably out there, but I'm too tired to go Googling right now.

RIP, Kenneth Appel. You did a bold and very good thing.