Re: [mizar] Another factor...

[Freek Wiedijk <freek@cs.kun.nl>]

Hello,

>>	http://megrez.mizar.org/ccl/state.html#report
>I'm going to count theorems.

So I'm through with counting:

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!

Freek