Formalizing the Gromov-Hausdorff space

TL;DR

This paper presents a formalization of the Gromov-Hausdorff space within the Lean proof assistant, highlighting the necessary departures from traditional informal definitions to achieve rigor.

Contribution

It provides the first detailed formalization of the Gromov-Hausdorff space in a proof assistant, clarifying the formalization process and necessary conceptual adjustments.

Findings

Successful formalization in Lean proof assistant

Clarification of differences between informal and formal definitions

Foundation for further formalized research in metric geometry

Abstract

The Gromov-Hausdorff space is usually defined in textbooks as "the space of all compact metric spaces up to isometry". We describe a formalization of this notion in the Lean proof assistant, insisting on how we need to depart from the usual informal viewpoint of mathematicians on this object to get a rigorous formalization.