Re: [math-fun] New proof of Four-Color Theorem
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
On Sun, 2 Oct 2005, dasimov@earthlink.net wrote:
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.)
http://www.math.gatech.edu/~thomas/FC/fourcolor.html (I am not sure if this is still uptodate, though). Helger
At 02:01 AM 10/2/2005, dasimov@earthlink.net, math-fun wrote:
It may, however, still be about as hard as ever for a human to verify that the original computer proof was valid. ...
That's true. But do you trust a human to be more accurate than a computer at those tedious details? I remember in the mid 80s when the office I was working in got its first computer. I told them to check some output. They started checking the computer's arithmetic. I said "No, you don't need to check the computer's addition - check to make sure you entered it correctly."
participants (3)
-
dasimov@earthlink.net -
Helger Lipmaa -
Jud McCranie