[FOM] Hersh on Flyspeck

[Timothy Y. Chow]

Back in January 2008, I 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.

Does anybody know if Hersh has commented publicly on the announcement of 
the completion of Flyspeck?  Obviously, he was wrong about the completion 
of the project.  Hersh can trivially ensure that Flyspeck will fail to be 
"universally" accepted, simply by refusing to accept it himself, but does 
he believe that significant numbers of mathematicians will continue to 
resist machine-verified formal proofs?

I'm not sure what Hersh has in mind by "definitively verifying the 
correctness of a proof," but I really don't believe that the mathematical 
community as a whole is any more skeptical about the proof of the Kepler 
conjecture than about, say, the proof of Fermat's Last Theorem or the 
Poincare Conjecture.  Does any FOM reader have anecdotal evidence to the 
contrary?

Tim

P.S. On a somewhat related note, I just learned (from Professor Joe 
Gallian) about the paper "A group theory of group theory" by Alma 
Steingart, which you can read here:

http://alum.mit.edu/www/tchow/steingart.pdf

Steingart takes a close look at the sociology of the proof of the 
classification of finite simple groups and arrives at conclusions that are 
somewhat similar to Hersh's philosophy of mathematics.