FOM: Length of formalizations

Piotr Rudnicki piotr at
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.

Piotr Rudnicki 

More information about the FOM mailing list