The Gromov-Hausdorff space, informally described as the space of all compact metric spaces up to isometry, requires careful set-theoretic treatment to formalize because naive quotient constructions over a proper class are not directly expressible in type-theoretic proof assistants.

The paper describes a formalization of the Gromov-Hausdorff space in the Lean proof assistant. It discusses where the informal mathematician's viewpoint must be adapted to produce a rigorous formalization, particularly around the set-theoretic issues of quotienting a type that is too large.

The Gromov-Hausdorff space is formalized in Lean, with the formalization contributed to mathlib. The work demonstrates how departures from standard informal mathematical presentations are sometimes necessary for rigorous formalization.