Re: [mizar] Another factor...

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

On Sat, Jan 18, 2003 at 10:33:11PM +0100, Freek Wiedijk wrote:

> If one compares "addressable items" (theorems and definitional
> theorems in MML versus numbered "items" - propositions,
> definitions, theorems, lemmas, etc. - in the book) then there
> are about 8 times as many if you only consider the WAYBEL
> series, or about 13 times as many if you also consider the
> YELLOW series.  (Maybe a reasonable number to remember is a
> factor of 10 :-))
> 
> That would mean that the MML would correspond to about 4000
> "human" theorems.  I think that's a surprisingly big number!

14 years will give some 285 "human" theorems a year.  For the number
of people involved it maybe a low or a high number as you like it.
However, most of the theorems are of the folklore type facts and too
frequently essential facts are missing.  I think that it would be
beneficial to the Mizar project if there were fewer loose experiments
like the the SCM, CIRCUIT (I participated in both) or BVFUNC series
and more systematic development of basic math.

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr