FOM: Length of formalizations

[Piotr Rudnicki]

Harvey Friedman, Tue Dec 28 10:33:24 1999, wrote:

> What do the results of Mizar so far indicate about the lengths of actual
> formalizations of deep mathematical proofs? Of that I am not sure, but I
> tend to think that Mizar is evidence that we are dealing with a linear
> phenomenon with manageable constant factor.

An answer to this question would require to set some criteria for
comparison and I do not know that extensive studies of the question
have been ever conducted for Mizar texts.  However, I can offer some
preliminary data.

There is an ongoing effort in Mizar to formalize "A Compendium of
Continuous Lattices" by G. Gierz et al., Springer 1980.  In 1997,
together with Cz. Bylinski, we formalized pages 105-108 of the book
about the Scott topology (the formalization of the earlier material
was available to us).  The text in the book includes definitions,
theorems with proofs and comments; it uses about 2000 tokens (words
and symbols).  The Mizar formalization uses about 15500 tokens.  About
4500 of these concern (simple) facts that in the book are not proved
but used.  Thus the 2000 tokens from the book required about 11000
tokens in the formalization.  (These numbers should be treated only as
a rough measure, they are based on what is meant by a token).  I am
in no position to judge how deep and complicated is the mathematics
involved but the length of the formalization was much smaller than we
initially expected.

The Mizar formalization is available at:

	http://mizar.uw.bialystok.pl/JFM/Vol9/waybel14.html

-- 
Piotr Rudnicki