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

[Mario Carneiro]

I cannot speak directly to the question of which formalization the QED
manifesto is referring to, but if you are looking for alternative
formalizations of those theorems, Metamath has a formalization of the
Banach Fixed Point theorem at http://us.metamath.org/mpegif/bfp.html .

Mario Carneiro

On Wed, Nov 26, 2014 at 10:33 AM, 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20141126/e1362e44/attachment.html>