[FOM] Question about theoretical physics

[joeshipman at aol.com]

I just reread the 1977 book "The Four-Color Problem: Assaults and Conquest", by Saaty and Kainen, which gives a very clear and thorough explanation of the AHK proof, and also looked at the original 139-page proof. It is clear that the second part of the proof, which involves showing the set of 1478 configurations is reducible, is easily  machine-verified except for putting the 1478 configurations into machine-readable form. Furthermore, the 1478 are a cutting-down of an original set of 1936 configurations, all of which were shown to be reducible by AHK, and it seems likely to me that if there had been any failure of unavoidability in the set of 1936, it would have been caught during the process of reducing to 1478. 

Therefore it seems fair to give AHK credit for having really proven the theorem.

However, the first part of the proof, which shows unavoidability, is not really satisfactory, because it does not give sufficient detail to allow for mechanical checking, even though computers were used to generate the unavoidable set. It appears that to check the proof by hand would require several hundred hours of very tedious work by an expert, and would not be possible for a non-expert. 

Therefore, I understand RSST's decision to reprove the theorem in such a way that the unavoidability part is also machine-checkable, but I also believe that the original AHK proof was probably adequately verified by the referees before it was published.

-- JS

-----Original Message-----
From: Joe Shipman <JoeShipman at aol.com>
To: tchow <tchow at alum.mit.edu>; Foundations of Mathematics <fom at cs.nyu.edu>
Sent: Wed, Mar 6, 2013 11:48 am
Subject: Re: [FOM] Question about theoretical physics


Thanks for the correction. I knew the RSST proof was well-documented but had not 
realized the original AHK proof had not been fully verified. Verifying the 
reducibility of the 1478 configurations in the AHK paper's "unavoidable set of 
reducible configurations" is straightforward if they are provided in a 
machine-readable form, and I'm surprised AKH did not do that. However, according 
to the RSST paper, it seems that the real obstacle was not the machine-aided 
verification of reducibility, but the "by hand" verification of unavoidability, 
which RSST gave up on.

Given this, I wonder if it is even correct to credit AKH with the proof. I would 
like to see an independent verification that AKH's 1478 configurations are 
unavoidable, or at least that they are unavoidable after a small number of 
clerical errors in drawing the configurations are fixed.

I would not deny AKH credit just because their proof of unavoidability is too 
tedious to be easily verified. 

However, if their original set of 1478 configurations must, even after 
correcting typos, be extended to a set of reducible configurations of larger 
cardinality, some of which had not been checked by AKH for reducibility, in 
order to be unavoidable, then I would declare that their proof had a gap and 
credit RSST with the first complete proof. (I know AKH had a larger set of 
verified-reducible configurations which they simplified for publication, and 
don't want to deny them credit if the published set of 1478 was only incomplete 
because of oversimplification.)

-- JS

Sent from my iPhone

On Mar 2, 2013, at 3:37 PM, "Timothy Y. Chow" <tchow at alum.mit.edu> wrote:

On Sat, 2 Mar 2013, Joe Shipman wrote:
> Tim's analogies to mathematics are on the right track but there are 
distinctions his examples need to reflect. The Appel-Haken-Koch proof was 
objectionable only because the calculations were too large to be verified by 
hand, but the documentation was always excellent so that it was easy both to 
verify the proof that the algorithm was correct, and to reproduce the 
calculation.

This is not quite accurate.  Though the use of a computer was what got all the 
tongues wagging, the most tedious part of the job for any potential verifier was 
checking all the little hand-drawn diagrams on the 400-page microfiche 
supplement to the paper.  I have heard that someone did make a heroic effort to 
try to verify everything, and in the process discovered lots of little bugs in 
the diagrams.  I believe that that verification effort was never carried out to 
completion.  When Robertson, Sanders, Seymour, and Thomas decided to take a 
crack at it, they eventually decided that it was easier to re-prove the result 
using the same general strategy, because checking the original proof (and fixing 
all the bugs) was just too painful.  The RSST proof *is* satisfactorily 
documented, and today we even have a Coq proof of the four-color theorem, thanks 
to Gonthier.  But I hesitate to say that the documentation of the original proof 
was "excellent."

Tim
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom

 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130306/57e4be31/attachment-0001.html>