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

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

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
>
> On Mon, 16 Apr 2007, Jesse Alama wrote:
>
> > Thought I'd forward this along to the mizar list, even though it
> > superficially has to do with Coq.  The web page mentioned in the 
> > message
> > refers to mizar.
> >
> > Jesse