[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] A quote
On Tue, Jan 13, 2004 at 11:07:50AM +0100, Freek Wiedijk wrote:
> >PR wrote:
> >However, Mizar library seems to be largest of such and I
> >think that building such a library is the main challenge,
>
> For me another challenge is to get formalization time down.
> I claim that currently it takes on average about one week to
> formalize one page from a math textbook. To develop
> technology that brings that time down to (say) one day,
> that's important too. Maybe even more important than the
> challenge you mention.
We have here a typical chicken and egg problem. Formalization takes
long time because the data base has holes and the database is puny as
adding to it takes long time.
I have recently finished proving the Wedderburn theorem. Proving the
theorem took about a week yet it generated about 100 lemmas to prove,
some of them of some substance, some of them utterly trivial. And
several months later they have been proved.
Of course that getting the formalization time down is a challenge but
a sizeable data base can be just what we need to meet this challenge.
Cheers,
--
Piotr Rudnicki CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr