FOM: Length of formalizations

[Andrej.Bauer@cs.cmu.edu]

TO MODERATOR:

I apologize for sending a previous message prematurely. My mail client
thinks Ctrl-S is "send" and I am used to Ctrl-S being "search" like in
Emacs. If it is not too late, please disregard the previous message and
publish this one instead. Thank you.

TO FOM:

I forget what the original motivation in this discussion was for
looking at lengths of proofs of "standard" mathematics, but if 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 proof 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.

  Definitions + Theorems about FOL = 39488 characters
                                   = 1311  lines of "code"

I doubt one could write an informal exposition in 39488 characters
about FOL that would cover everything that is in Isabelle FOL package.
This is not too surprising since Isabelle has built-in theorem proving 
strategies for first-order classical logic, so humans don't have to
explain much how to prove pure FOL theorems.

The situation with ZF set theory (Axiom of Choice is there, too) is
a bit different:

  Definitions + Theorems about ZF = 493115 characters
                                  = 15514  lines of "code"

This much text would correspond to a thick book, or a fairly
sophisticated application (it's about the size of the popular Auctex
package for emacs, for example). What is covered in the Isabelle ZF
package? Other than basic axioms, definitions, facts about subsets,
functions and relations, etc, we also have:

 - well-founded recursion
 - ordinal numbers (basic definitions and facts)
 - Schroeder-Bernstein Theorem
 - natural numbers
 - epsilon induction and recursion
 - properties of finite sets and induction principles for them
 - basic properties of orders (partial, linear, well-order)
 - cardinals and basic cardinal arithmetic
 - Axiom of Choice, Zorn Lemma

I probably left out some other non-trivial subjects. I believe various
people have formalized even more than that. For details have a look at
http://isabelle.in.tum.de/library/ZF/

Isabelle theories are divided into two parts. The first part consists
of definitions and statements of theorems, and the second part
consists of hints on how to prove the theorems. In the ZF package
about 8% of the code goes to the first part and the rest goes to the
second part.

Unfortunately Isabelle does not generate proofs. It just verifies them 
but it never stores them or outputs them. So we do not know how large
the actual formal proofs would actually be. They cannot be too large
because Isabelle generates and verifies the whole FOL+ZF theory in
less than 20 minutes on my desktop.

When we embark on formalizing all of existing mathematics (and there's
no 'if' about this in my opinion) we are not going to write formal
proofs by hand, and neither are we going to be able to make programs
that will do everything for us. Instead, we are going to provide
advice to computers on how to solve problems, like in Isabelle. That
is why looking at the size of advice needed is sensible, if somewhat
crude, measure of how difficult this task is going to be. It seems to
me that there definitely is at most a constant blow-up when we pass from
informal text to formalized definitions and advice. I base this opinion
on the above numbers and the fact that in Isabelle the complicated
theorems require just as much advice as the easy ones. Rather, they
require carefully constructed Lemmas, just like in an informal text.
Future proof checkers are likely to be much better than Isabelle.


Andrej Bauer

  Ph.D. student in Pure and Applied Logic
  School of Computer Science
  Carnegie Mellon University
  Andrej.Bauer at andrej.com