[FOM] Hersh on Flyspeck

[Timothy Y. Chow]

In the introduction to his delightful anthology, "18 Unconventional Essays 
on the Nature of Mathematics," Reuben Hersh states, regarding the Flyspeck 
project of Thomas Hales, that he does not know anyone who either believes 
that the project will be completed or that, even if claimed to be 
complete, it will be universally accepted as definitively verifying the 
correctness of the proof.

This, to me, is quite an astounding claim.  It is one thing to believe 
that the project will never be completed, but it is quite another to say 
that he *does not know anyone who believes otherwise*!  (Including Hales, 
even?)  Just how widespread is the belief that Flyspeck will never be 
completed?

Part of the issue is that Hersh misunderstands Hales's estimate of the 
work required to complete Flyspeck, which is something like 20 
person-years.  Hersh exaggerates this to "hundreds of people working for 
20 years."

The part about universal acceptance is more interesting.  With a 
sufficiently literal interpretation of "universal," it is not universally 
accepted that angle trisection is impossible, as anyone who has dealt with 
mathematical cranks knows.  But presumably Hersh means to claim something 
stronger---that (as I would phrase it) the Formalization Thesis is false 
in this particular instance.  That is, there will be substantial 
disagreement as to whether the formal theorem verified by HOL Light 
faithfully represents what we understand by "The Kepler Conjecture."

Do any of the opponents of the Formalization Thesis (as I stated it) 
believe that, even if Flyspeck is completed as planned, there will be no 
consensus among ("non-crank") mathematicians regarding whether the formal 
theorem accurately expresses the Kepler Conjecture?

Tim