[FOM] Formalisation of the Banach fixed point theorem and the Picard-Lindelöf theorem
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:
> 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.
> Marco Maggesi
> FOM mailing list
> FOM at cs.nyu.edu
More information about the FOM