[mizar] Another factor...

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

Hello,

As you might know, I like "human metrics" of proof checking.
So I "measured" the following two factors (current state of
the art, it should become better at some point! :-)):

  size of Mizar / size of LaTeX ~= 4 kB/kB

  time to Mizar / size of textbook ~= 1 work week/page

But there's a third factor I'm curious after: the number
of "lemmas" (things that gets a label in a Mizar abstract)
versus the number of "propositions" in a textbook.  I'm fairly
sure it's not 1-to-1 :-)

So I can compare:

  <http://www.cs.kun.nl/~freek/factor/waybel14.ps.gz>
  <http://www.cs.kun.nl/~freek/factor/waybel14.miz>

There it's 46 to 5, which is about 9.

But I wonder what the factor is for the whole "waybel/yellow"
translation up to now.  Does anyone have some data about
this?  Order of magnitude is fine for me.  Also a description
of which articles correspond to what part of the book would
be okay (I can count the propositions in the book myself.)

Freek