Re: [mizar] Good news from a mathematician

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

On Tue, Jan 13, 2004 at 10:18:19AM +0100, Freek Wiedijk wrote:
> Hi Piotr,
> 
> >If anyone reading this has known about the following webpage
> >before and did not post it here then they better have some
> >excuse: [...]
> 
> _I_ knew about it...  My excuse is that I thought that
> everyone already knew about it.

Of course, I should _have_ known about it.

> Okay, so just to be sure: you _have_ heard of the Logosphere
> initiative, haven't you?
> 
> 	http://www.logosphere.org/

Yes, I did, didn't they present the stuff in Edinburgh in November.
The project sounds as nebulous as all these Logical Frameworks, tons
of machinery and somehow the product is difficult to detect.


> >Are we joining the effort? 
> 
> They can't use Mizar, as the proof is _very_ computational
> (it took a Sun _months_ of calculation.)  It's similar to the
> four color theorem.

Hmm.  I have had a coursory look thorugh the abridged version of the
proof and it looks that besides the optimization problems there are
many theorems amenable for Mizar treatment.

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