  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.
