Formalizing the Gromov-Hausdorff Space

EasyChair Preprint 6179

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.

Keyphrases: Gromov-Hausdorff space, Lean, formalization

@booklet{EasyChair:6179,
  author    = {Sébastien Gouëzel},
  title     = {Formalizing the Gromov-Hausdorff Space},
  howpublished = {EasyChair Preprint 6179},
  year      = {EasyChair, 2021}}