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

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi,

first of all, I should have written "extremely large and overambitious 
project" instead of just "large and ambitious" when talking about formal 
proof of Poincare's conjecture. Here is the 500-pages long "systematic 
map" by John Morgan & Gang Tian: http://www.arxiv.org/ps/math/0607607 . 
To speak a bit rationally, I think that just developing basic differential 
geometry, and a bit more of Riemannian geometry would be fairly useful 
work.

And I also very much agree with Andrzej: the reason for mentioning such a 
challenge is to get some idea about how far we currently are from it, and 
to try to figure out what it would take to do it with the current state of 
art (and perhaps start to think about what are the largest bottlenecks 
of the current state of art). It is true that having "the big project" in 
the back of one's mind could lead people to doing their formalizations in 
a more re-usable way, and to realize that the whole library and its 
maximal utility is the ultimate target (not a huge number of dissociated 
articles largely copying from each other, and hardly useful for anything).

Best,
Josef


On Fri, 20 Apr 2007, shidama yasunari wrote:

> Dear Prof.Andrzej Trybulec,
>
>
> > So, if we choose the formalization Perelman's proof as a challenge, who
> > is ready to join the effort?
>
>  Of course, we will completely cooperate in it.  However, we need a 
> systematic map. A lot of tools are necessary for it. 
> Regards,
> Yasunari Shidama
>
>
> > From: Andrzej Trybulec <trybulec@math.uwb.edu.pl>
> > 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: 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] 
> 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