Re: [mizar] Good news from a mathematician

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

Dear Piotr,

>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.

Freek