Date: Fri, 20 Apr 2007 12:10:28 +0200
The systematic development of MML is most important and looking for
Graal is no so good idea. So, I support the Yasunaru Shidama approach.
On the other hand, challenges are important, too. Not even of propaganda
reason, but they enable to anicipate how the formalization should be
done. I like Josef's idea. Whilst the four color problem seems to be
marginal in topology (who needs it?), the Poicare hypothesis is quite
important. I sort of remenber papers of the classification of
3-dimensional manifolds done modulo the Poincare hypothesis. And I do
not know what is the status of the Zeeman hypothesis (the product of
contractible 2-dimensional polyedron by the [.0,1.] segment is
collapsible). It seems a bit stronger.
So, if we choose the formalization Perelman's proof as a challenge, who
is ready to join the effort?
Regards,
Andrzej
shidama yasunari wrote:
> Dear Prof.Josef Urban
>
> We pay a huge effort for such the future plans now and are
> constructing the fundamental library. Calculus,Function analysis
> ...........
> There is no last point. :+)
>
> Yours very sincerely.
> Yasunari Shidama
>
>
>
>> From: Josef Urban <urban@ktilinux.ms.mff.cuni.cz>
>> Reply-To: mizar-forum@mizar.uwb.edu.pl
>> To: mizar-forum@mizar.uwb.edu.pl
>> Subject: Re: [mizar] [gmane.science.mathematics.logic.coq.club]
>
> curve in Coq
>
>> Date: Mon, 16 Apr 2007 18:09:13 +0200 (CEST)
>>
>>
>> Speaking about large ambitious projects, Perelman's proof of
>> Poincare's conjecture would be another. And it might push the
>> formalization field quite a bit, because of the amount of modern
>> geometry involved there.
>>
>> Josef