FOM: Length of formalizations

[Piotr Rudnicki]

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.

-- 
Piotr Rudnicki