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

[Josef Urban]

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