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

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

Dear Prof. Shidama,

it's good to hear about these projects. All of them will make the library 
more complete with what is considered to be the basic mathematical 
apparatus. I guess one reasonable suggestion for a goal which could direct 
these efforts a bit could be e.g the Stokes' theorem.

Best,
Josef

On Sat, 21 Apr 2007, shidama yasunari wrote:

> 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