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

[Marco Maggesi]

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