[FOM] Re: The Role of Formalization

[Timothy Y. Chow]

henriknordmark at mac.com wrote:
> Is there a need for a repertoire of formal symbolic proofs? Is it in 
> some sense mathematically interesting to provide symbolic proofs of our 
> current mathematical knowledge? Is it worth investing time and money 
> for such an endeavor? Would we be able to gain any new insights by 
> doing this? Will future generations in any way profit from having a 
> repertoire of symbolic proofs at their disposal?

In case anyone on this list is not already aware of the Flyspeck project
( http://www.math.pitt.edu/~thales/flyspeck ), I'd like to mention that
Thomas Hales is an example of an outstanding mainstream mathematician who
thinks that the answer is yes.

On the other end of the spectrum, I expect that most (though perhaps not
all) FOMers recall the Jaffe-Quinn-Thurston-et al. debate about
"theoretical mathematics" about ten years ago.  (Exact references below
for those who are interested.)  I believe I read a joke in Krantz's
"Mathematical Apocrypha" that "Thurston proved that you can win a Fields
Medal without ever proving a theorem, and Witten proved that you can win a
Fields Medal without ever stating a theorem."  Of course this joke is more
than just a wild exaggeration; it's blatantly false.  Still, it's true
that folks like Witten have produced a ton of non-rigorous work that is
judged by a significant fraction of mathematicians to be *mathematics*.
Here the question is whether even *rigorous* proofs, let alone formal
symbolic proofs, are worth working on; the general consensus nowadays
among mathematicians is yes, but I wonder if even this seemingly
sacrosanct principle might eventually be overthrown.  I doubt it, but
who knows?

Somewhere in between the above "extremes" is the classification of finite
simple groups.  To some it might have come as a surprise when Aschbacher
and Smith announced that the classification was not proved back in the
early 80's but was only fully proved with the recent public release of
their 1200-page manuscript on quasithin groups.  It's a bit strange,
isn't it, that much of the mathematical community blithely ignored a
1200-page gap for 20 years?  To me at least, this suggests that as proofs
of this size get more common, we should no longer be so cocksure that we
are able to detect all significant gaps without machine assistance 
(especially if there is no social reward for checking the correctness of
someone else's complicated proof).  So I predict that the next 50 years 
will see an increase in the importance of projects like Flyspeck.

Tim



[1] math.HO/9307227.
Arthur Jaffe, Frank Quinn. "_Theoretical Mathematics_: Toward a Cultural
Synthesis of Mathematics and Theoretical Physics". 13 pages. Bull. Amer.
Math. Soc. (N.S.) 29 (1993) 1-13.

[2] math.HO/9404236.
William P. Thurston. "On Proof and Progress in Mathematics". 17 pages.
Bull. Amer. Math. Soc. (N.S.) 30 (1994) 161-177.

[3] math.HO/9404229.
Michael Atiyah, Armand Borel, G. J. Chaitin, Daniel Friedan, James Glimm,
Jeremy J. Gray, Morris W. Hirsch, Saunder MacLane, Benoit B. Mandelbrot,
David Ruelle, Albert Schwarz, Karen Uhlenbeck, Rene Thom, Edward Witten,
Christopher Zeeman. "Responses to _Theoretical Mathematics_: Toward a
Cultural Synthesis of Mathematics and Theoretical Physics", by A. Jaffe
and F. Quinn. 30 pages. Bull. Amer. Math. Soc. (N.S.) 30 (1994) 178-207.
 
[4] math.HO/9404231.
Arthur Jaffe, Frank Quinn. Response to Comments on _Theoretical
Mathematics_". 4 pages. Bull. Amer. Math. Soc. (N.S.) 30 (1994) 208-211.