[FOM] Hersh on Flyspeck

[Dana Scott]

I wrote Hales to ask his reaction.  Just as with the Four Color
Theorem, there seems to be considerable misunderstanding about
what computer-aided proofs do and how they work.

Begin forwarded message from Thomas Hales <tchales at gmail.com>:

> I was able to find and read Hersh's essay by googling the phrase
> "Project Flyspeck is expected".  I do not belong to the FOM list, but
> can give this response that you are welcome to share.
>
> I am quite certain the project will be completed, and yet I am quite
> happy to hear that Hersh and his friends have their doubts.  The
> more doubters there are, the sweeter the success, when it happens.
>
> Hersh concludes "Such a story undermines our faith that mathematical
> proof will remain as we have always thought of it–that after
> reasonable time and effort, its correctness must be definitely
> decidable by unanimous consensus of competent specialists."
> The doctrines of various religions are decided by the
> unanimous consensus of their ruling bodies.  This also seems to
> be his standard of mathematical proof.
>
> Formal methods give a scientific standard of certification that does
> not require the unanimous consent of authorities.  It is a scientific
> standard in the sense that we could calculate the probability of a
> false certification of a proof, by looking at defect rates in software
> and so forth.  As technology improves, we can hope to make that
> probability so small that it no longer a practical concern.
>
> From my view, the Flyspeck project appears to be on schedule.  There
> are three significant pieces of code in the proof of Kepler.  The
> first has now been completely verified by Bauer and Nipkow (on the
> classification of tame graphs).  Obua is scheduled to defend his  
> thesis
> in the early summer of 2008 on the second piece (linear programming).
>
> This does not do the full verification of the second piece of code,
> but it brings it within grasp.  Two other graduate students McLaughlin
> and Zumkeller are working very hard on the third piece of computer  
> code.
> If progress continues at this rate, I think that it is reasonable to
> expect the code to be fully verified within the next few years.
>
> I have spent much of this last year rewriting the text part of the
> proof in a formalization-friendly way.  The revised text contains all
> of the relevant background material, starting with basic trig.  See
> the flyspeck project page (http://code.google.com/p/flyspeck/) for
> details about the project.
>
> John Harrison <johnh at ichips.intel.com> continues to add features to
> HOL Light that simplify the project.  The text is no more than 6-8
> work-years from completion. I have one graduate student at Pitt who is
> now working with me on this and I have just recruited (at least) one
> more student from the course I taught in Hanoi this fall.