[FOM] Hersh on Flyspeck
Tjark Weber
tjark.weber at gmx.de
Sat Jan 12 20:30:48 EST 2008
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
More information about the FOM
mailing list