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

Josef Urban josef.urban at gmail.com
Thu Nov 27 02:55:28 EST 2014

I can see Banach done in Mizar in 1991 by  Alicia de la Cruz:
(for compact spaces),
(for complete spaces). So this was before QED.

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

More information about the FOM mailing list