Re: [mizar] Good news from a mathematician

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

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.

Okay, so just to be sure: you _have_ heard of the Logosphere
initiative, haven't you?

	http://www.logosphere.org/

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

Freek