[FOM] Formalisation of the Banach fixed point theorem and the Picard-Lindelöf theorem

[Marco Maggesi]

Thank you Josef for your indication.

I tried to look in the Mizar library myself but I wasn't able to find
anything. I spent a little more time to see if  also the Picard-Lindelöf
theorem is in the Mizar library, but, perhaps because I have a very limited
understanding of the Mizar language, I didn't find anything so far.

I looked also in other libraries (e.g. Nurpl), but with no luck.

Marco

Il giorno Fri Nov 28 2014 at 11:24:48 PM Josef Urban <josef.urban at gmail.com>
ha scritto:

> I can see Banach done in Mizar in 1991 by  Alicia de la Cruz:
> http://mizar.cs.ualberta.ca/~mptp/8.1.03_5.23.1213/html/ali2.html#T1
> (for compact spaces),
> http://mizar.cs.ualberta.ca/~mptp/8.1.03_5.23.1213/html/tbsp_1.html#T7
> (for complete spaces). So this was before QED.
> Josef
>
> On Wed, Nov 26, 2014 at 4:33 PM, Marco Maggesi <maggesi at math.unifi.it>
> wrote:
> > Hi,
> >
> > I found in the QED Manifesto (http://www.cs.ru.nl/~freek/qed/qed.html)
> > a list of computer checked theorems (reported in "Reply to Objection
> > 11", p.6 on my copy) where, among other things, it cites the Banach
> > fixed point theorem and the Picard-Lindelöf theorem.
> >
> > This means that, at that time, 1994, those theorems were already
> > mechanically checked with a theorem prover.
> >
> > Can someone say to which formalisations the QED Manifesto alludes?
> >
> > My personal interest in this questions comes from the fact that I
> > recently completed the proof of the same theorems in HOL Light
> > (https://bitbucket.org/maggesi/metric/) thus I would be interested for
> > curiosity and also to make a comparison.
> >
> > Thanks,
> > Marco Maggesi
> > _______________________________________________
> > FOM mailing list
> > FOM at cs.nyu.edu
> > http://www.cs.nyu.edu/mailman/listinfo/fom
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20141202/71d7bd48/attachment-0001.html>