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

[Marco Maggesi]

Dear Mario,

thank you very much for your answer.  I wasn't aware about this
formalisation in Metamath.

I found two other recent related works.  One in Isabelle/HOL:

Fabian Immler, Johannes Hölzl,
"Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL"
Interactive Theorem Proving
Lecture Notes in Computer Science Volume 7406, 2012, pp 377-392

The other in Coq:

Evgeny Makarov, Bas Spitters,
"The Picard Algorithm for Ordinary Differential Equations in Coq"
Interactive Theorem Proving
Lecture Notes in Computer Science Volume 7998, 2013, pp 463-468

Marco



2014-11-26 22:53 GMT+01:00 Mario Carneiro <di.gama at gmail.com>:
> 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
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>