[FOM] Question about theoretical physics
joeshipman at aol.com
joeshipman at aol.com
Wed Mar 6 18:17:26 EST 2013
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>
More information about the FOM
mailing list