[FOM] Hersh on Flyspeck
dana.scott at cs.cmu.edu
Tue Jan 15 13:33:47 EST 2008
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
> 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
> 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.
More information about the FOM