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

["shidama yasunari" <shirodanuki@hotmail.com>]

Dear Prof.Josef Urban,
　　The most basic, classic tool of differential geometry might be calculus 
of the multivariable.　
These are   few in MML.　For instance, the library of the partial 
derivative operator
(partial derivatives for PartFunc of REAL n ,REAL  ) was  contributed  as 
PDIFF_1 two weeks ago.
 We are making the library of this higher degree derivative  now.
Making the multivariable version of Riemann integra started  last week.
And the library of calculus for the complex functions had started last 
month.

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: Fri, 20 Apr 2007 18:13:16 +0200 (CEST)
>
>
> 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