Re: [mizar] A quote

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi Freek,

> >Formalization takes long time because the data base has
> >holes
> 
> I'm not sure that's the main problem.  Generally in the
> little experiments that I do I can find the lemmas that I'm
> looking for... after a long time searching for them and
> trying to get the typing to work and everything.

You may be right at the moment, but I believe that in the long run, the 
searching capabilities will be one of the main arguments _for_ formalizing 
mathematics.
Look how good Google is in searching natural language - and 
formalized mathematics has a great advantage over it - it has semantics.
So if inductive methods (like Google's) fail, we can still use deductive 
(e.g. provers) or combine them.

Josef