# Marco Maggesi *"A formalization of metric spaces in HOL Light"*

Talk at GnCS
2017, Pescara 8th-11th February 2017
## Abstract

We present a computer formalization of metric spaces in the HOL
Light theorem prover. Basic results of the theory of complete metric
spaces are provided, including the Banach Fixed-Point Theorem, the
Baire Category Theorem and the completeness of the space of continuous
bounded functions. A decision procedure for a fragment of the
elementary theory of metric spaces is also implemented. As an
application, the Picard-LindelĂ¶f theorem on the existence of the
solutions of ordinary differential equations is proved by using the
well-known argument which reposes to the Banach theorem.

## Slides

PDF file of the slides