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