[FOM] Question about theoretical physics

[Timothy Y. Chow]

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