Re: [mizar] [gmane.science.mathematics.logic.coq.club] Elliptic curve in Coq

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

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] Elliptic 
> 
> 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