[FOM] Hersh on Flyspeck

[Tjark Weber]

Tim,

On Friday 11 January 2008 03:22, Timothy Y. Chow wrote:
> 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.
>
> [...] 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?

of course I can't read Hersh's mind, but I think you are misunderstanding him 
here.  Presumably his above claim about the Flyspeck project has little to do 
with the Formalization Thesis.  The (statement of the) formal theorem that 
will be verified in the Flyspeck project is relatively short and simple.  
There should be little reason for disagreement as to whether that theorem 
really is the one representing the "Kepler conjecture".  To my knowledge, no 
serious mathematician has claimed that Hales proved the wrong statement.

However, Hales' proof of the Kepler conjecture (if I understand the situation 
correctly) was so complex that the reviewers eventually gave up on verifiying 
the proof.  The question is not whether Hales proved the right statement, but 
whether his proof is correct.

So if an extremely complex journal proof of the Kepler conjecture does not 
convince us that the conjecture holds (because there may be an error hidden 
somewhere in the proof), will a software tool like HOL Light convince us when 
it ultimately says "This statement is proven."?  I believe Hersh simply means 
that this will not "be universally accepted as definitively verifying the 
correctness of the proof" either.

Tjark