[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Another factor...
Dear Piotr,
> http://www.cs.ualberta.ca/~piotr/02JAR/
> http://www.cs.ualberta.ca/~piotr/02JAR/old/
> http://megrez.mizar.org/ccl/state.html#report
Thanks for the links! I'm going to count theorems.
>The measure which you are suggesting may be misleading I am
>afraid if taken at the face value as in principle it was
>possible to have such translation almost at the 1-1 level.
Sure! It depends on both the styles of the book and of the
person doing the formalization. But that's good enough for
me, I just was interested in a rough estimate.
I would like to be able to say "the MML contains on the order
of so-and-so many theorems" and then be talking about usual
theorems instead of about _Mizar_ theorems (which are a bit
more light-weight, it seems to me.) So there are about
40,000 Mizar theorems there, right? So how many _book_
theorems would that be? :-)
Also, if you're going to do the translation at the 1-1 level
you will need to duplicate proofs a lot, because you cannot
refer to "light" lemmas anymore (the ones that won't be in
the book). So I fear the possibility is not really a
practical one.
Freek