[math-fun] New proof of Four-Color Theorem
As is well-known, the four-color theorem was proved about 1977, making heavy use of computers. And since then, minor errors were fixed and the computer part of the proof was simplified -- but the proof still relied heavily on computer verification. Now it appears that a new proof has been found, not relying on computers, that has been fully (human-) verified. This new proof is by a mathematician named Georges Gonthier. Thomas Hales (whose own 1998 proof of the Kepler conjecture relies heavily on computers) will speak on this new proof at Swarthmore College on Wed., Oct. 5, at 4:30 pm. Here is his abstract: << The four-color theorem states that any map can be colored with four colors in such a way that adjacent countries do not receive the same color. This theorem is one of the most famous math problems ever to be solved by computer. Last year, Georges Gonthier gave a completely formal proof of the four-color theorem. This means that every step of the proof has now been carefully checked all the way down to the fundamental axioms of mathematics. I will describe Gonthier's project and explain how it relates to my current work on packing spheres.
--Dan
At 12:20 AM 10/2/2005, dasimov@earthlink.net, math-fun 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.
The abstract doesn't support the description of the new proof as human verified. Rich -----Original Message----- From: math-fun-bounces+rschroe=sandia.gov@mailman.xmission.com on behalf of dasimov@earthlink.net Sent: Sat 10/1/2005 10:20 PM To: math-fun@mailman.xmission.com Subject: [math-fun] New proof of Four-Color Theorem As is well-known, the four-color theorem was proved about 1977, making heavy use of computers. And since then, minor errors were fixed and the computer part of the proof was simplified -- but the proof still relied heavily on computer verification. Now it appears that a new proof has been found, not relying on computers, that has been fully (human-) verified. This new proof is by a mathematician named Georges Gonthier. Thomas Hales (whose own 1998 proof of the Kepler conjecture relies heavily on computers) will speak on this new proof at Swarthmore College on Wed., Oct. 5, at 4:30 pm. Here is his abstract: << The four-color theorem states that any map can be colored with four colors in such a way that adjacent countries do not receive the same color. This theorem is one of the most famous math problems ever to be solved by computer. Last year, Georges Gonthier gave a completely formal proof of the four-color theorem. This means that every step of the proof has now been carefully checked all the way down to the fundamental axioms of mathematics. I will describe Gonthier's project and explain how it relates to my current work on packing spheres.
--Dan _______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
On Sunday 02 October 2005 06:59, Rich Schroeppel wrote:
The abstract doesn't support the description of the new proof as human verified.
Unless things have changed since last December (always possible, I guess), Gonthier's proof is still computerized. What's different from the Appel/Haken proof is that all the steps have been made explicit and checked using an automated proof checker. So now, instead of having to trust a special-purpose 4-colour-theorem-analysing program and check some material in ordinary mathematical language, you have to trust a general-purpose proof checker. Gonthier's proof is an adaptation of the one of Robertson et al, which in turn is a streamlined version of the Appel/Haken one. Gonthier's home page at Microsoft Research is http://research.microsoft.com/~gonthier/ and there you can find a paper describing the proof, and even the proof itself. -- g
participants (4)
-
dasimov＠earthlink.net -
Gareth McCaughan -
Jud McCranie -
Schroeppel, Richard