Jud writes: << (I wrote):
As is well-known, the four-color theorem was proved about 1977, making heavy use of computers.
Heavy use for that time - about 1200 hours on an IBM 360. I assume that is the total CPU time and not just the time it was in the machine on a time-sharing basis. Interestingly, the equivalent computing on a typical modern desktop computer would be on the order of 10 minutes. Seconds on a modern supercomputer.
Aha -- thanks for pointing this out. It may, however, still be about as hard as ever for a human to verify that the original computer proof was valid. The more recent (mid '80s ?) improvment on the original proof would, I think, also be deemed hard to verify the correctness of the computer aspect of the proof. (I suspect that the correctness of at least the improved version is generally believed to now be human-verified, but am not sure of this.) --Dan