FOM: Length of formalizations

[Andrzej Trybulec]

On Thu, 13 Jan 2000 Andrej.Bauer at cs.cmu.edu wrote:

....

> 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.

Interesting.

The similar distinction is in Mizar. The whole text is called an article,
the statement of definitions and theorems is called the abstract of it.
In abstracts the proofs, lemmas, private concepts are removed, what
remains may be used in other articles.

The whole library (621 articles) is about 47 MBytes (46,850,843 Bytes)
and the abstracts 7 Mbytes (6,579,520 Bytes). Therefore the first part
is 14%, a bit better than in Isabelle :-)

> 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.

Mizar verifies the whole library in 1,5 hour (the Linux platform, 8 hours
under Windows). Again, the parameter is virtually the same.

> 
> 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. 

This I do not understand. Why do not write proofs by hand if it is 
comparable, if not a smaller effort that providing the hints to prover?

It is like supervising a Master Thesis for a not very able student. It
would be easier to write the Thesis, but in this case we unfortunately may
not do it.

>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.

The ratio of the "ouput" in the whole text is an interesting parameter
because we can compute it (the blowup factor is somewhat misty concept),
and the length of output is apparently the same as in the informal text.

It seems that the ratio is similar in the systems with completely
different approach. Michel Sintzoff told me, few years ago,  that is
virtually the same in Nuprl, if I recall. What about LEGO or Coq? The
Boyer Moore prover?

Andrzej Trybulec