Re: [mizar] Another factor...

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

Freek,

how did you count theorems like theorem 4.2 of section "Meet Continuous
Lattices" (CCL)? It is formalized in waybel_2:38 .. 55 (18 Mizar
theorems).

Artur


On Sat, 18 Jan 2003, Freek Wiedijk wrote:

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


=======================================

Artur Kornilowicz               e-mail: arturk@math.uwb.edu.pl

Dept. of Applied Logic          http://math.uwb.edu.pl/~arturk/
Institute of Computer Science   fax. +48 (85) 745-7662
University of Bialystok         tel. +48 (85) 745-7559 (office)
Sosnowa 64                           +48 (85) 651-6193 (home)
15-887 Bialystok, Poland