FOM: Length of formalizations
piotr at cs.ualberta.ca
Tue Jan 18 14:03:33 EST 2000
Harvey Friedman, 13 Jan 2000, wrote:
> Of course, the next question is what happends with more far ranging animals
> like, say, Rudin's Undergarduate Real Analysis Text? Or Landau's
> Foundations of Analysis? Can you handle a text that is currently used in
> the undergraduate mathematics curriculum? Are we going to get away with a
> modest constant factor blowup?
For the record:
Landau's "Grundlagen der Analysis" were formalized and checked in AUTOMATH
by L. S. van Benthem Jutting during the years 1968-1975. (Mathematical
Centre Tracts 83, Amsterdam 1979).
Jutting reported the blow up factor somewhere bewtween 3.8 and 6.4 depending
on the chapter of the book.
I believe that with current technology we can handle many of undergraduate books,
at least small scale experiments (by many people) seem to confirm my belief.
More information about the FOM