[FOM] Question about theoretical physics

[Joe Shipman]

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