FOM: Length of formalizations

[Andrej.Bauer@cs.cmu.edu]

I forget what the original motivation in this discussion was for looking
at lengths of proofs of "standard" mathematics, but it the motivation
is to find out whether it is feasible to actually formalize "standard"
mathematics then there is another useful point of reference, namely the
amount of information that has to be provided to a proof-checker in
order for it to be able to verify theorems and their proofs. Strictly
speaking, such hints are not proofs, but the proof checker can
efficiently generate proofs from them.

As an example, we can look at the Isabelle theorem checker developed by
Lary Paulson and others (http://isabelle.in.tum.de/). This is a generic
theorem checker that can handle various kinds of logic. A large body of
mathematics has been formalized in Isabelle. The audience on this
mailing list will probably appreciate most the numbers involving
classical first-order logic and ZF set theory. These theories come with
the standard distribution of Isabelle and you can have a look at them at
http://isabelle.in.tum.de/library/FOL/ and
http://isabelle.in.tum.de/library/ZF/

Here are some numbers to ponder: