Re: [mizar] Good news from a mathematician

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

On Tue, Jan 13, 2004 at 08:31:49PM +0100, Freek Wiedijk wrote:

> >I have had a cursory look through the abridged version of
> >the proof and it looks that besides the optimization
> >problems there are many theorems amenable for Mizar
> >treatment.
> 
> But if you check _parts_ in Mizar, but other parts in another
> system, then fitting things together doesn't seem trivial for
> me.  It seems to me that you can easily confuse yourself and
> introduce mistakes that way.
> 
> Besides they would have to learn two systems, instead of one.

Sure, but Hales is aiming at a 20 years of effort, at such time scale combining
two systems does not seems like an obstacle.

I have to look more into his proofs.  I suspect that the validity of
the stuff amenable for mizaring is not in question and thus there is
little interest.  How HOL can help more with the optimization problems than
Mizar? I do not know.  Does anybody?


-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr