The Gromov-Hausdorf 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. The Gromov-Hausdorf space is the space of all nonempty compact metric spaces up to isometry. It has been introduced by Gromov in [1], and plays now an important role in branches of geometry and probability theory. Its intricate nature of a space of equivalence classes of spaces gives rise to interesting formalization questions, both from the point of view of the interface with the rest of the library and on design choices for definitions and proofs. This text is devoted to a discussion of these issues: it describes a formalization of the main features of the Gromov-Hausdorf space in the Lean proof assistant, developed at Microsoft Research by Leonardo de Moura [2], within the library mathlib [3]. This text is written with two audiences in mind: it can be read by curious mathematicians who want to learn the basics of the Gromov-Hausdorf space, and by formalizers who want to learn about the challenges raised by the formalization of an unusual mathematical object such as this one. It should be reasonably self-contained. In Section 1, we give a purely mathematical description of the Gromov-Hausdorf space and its salient features. In Section 2, we give an overview of our formalization. The last three sections are devoted to specific interesting points that were raised during this formalization. More specifically, Section 3 discusses the possible choices of definition for the Gromov-Hausdorf space. Section 4 explains how preexisting gaps in the mathlib library had to be filled to show that the Gromov-Hausdorf distance is realized. Section 5 focuses on a particularly subtle inductive construction involved in the proof of the completeness of the Gromov-Hausdorf space, and the shortcomings of Lean 3 that had to be circumvented to formalize it.
In this paragraph, we give a quick overview on the Gromov-Hausdorf space as presented in mathematics textbooks. See for instance [4, Section 7.3] or [5, Section 10.1].
Given two nonempty bounded subsets and of a metric space , there is a way to tell how close these are, as subsets of , through their Hausdorf distance (, ). It is the infimum of those such that is included in the -neighborhood of (i.e., the set of points within distance at most of a point in ) and is included in the -neighborhood of . This is finite as and are bounded and nonempty, and zero if and only if and have the same closure. In particular, induces a distance on the space of nonempty bounded closed subsets of , and also on the space of its nonempty compact subsets. This distance is very well behaved: ( , ) is complete (resp. second-countable, resp. compact) if is.
Much more recently, Gromov has introduced in [
Definition 1.1. Let and be two nonempty compact metric spaces. Their Gromov-Hausdorf distance (, ) is the infimum of ′ (′, ′) over all metric spaces ′ and all subsets ′ and ′ of ′ which are isometric respectively to and .
Note that the infimum in this definition makes sense: it is always possible to embed isometrically and in a common metric space (for instance by putting a suitable distance on the disjoint union of and ).
Let ℋ denote the “space” of nonempty compact metric spaces up to isometry. There is a set-theoretic dificulty here, to which we will come back in Section 3 but that we will ignore for now.
The basic result in the theory is the following theorem, which we have formalized in the Lean proof assistant as part of the mathlib library.
Theorem 1.2. The Gromov-Hausdorf distance is indeed a distance on ℋ. With this distance, ℋ is a complete second countable metric space.
Let us highlight two important points in this theorem that will be relevant later on. • If two spaces are at distance zero, the theorem asserts that they are isometric. This is not obvious as the Gromov-Hausdorf distance is defined as an infimum. This result follows from the more general fact that the Gromov-Hausdorf distance between two spaces and is always realized, i.e., the aforementioned infimum is in fact a minimum. To prove this, one should construct a metric space ′ and two isometric embeddings : → ′ and : → ′ with ′ ( (), ( )) = (, ). • Given a Cauchy sequence of compact metric spaces (for instance a sequence such that (, +1) ≤ 2− ), the theorem asserts that there exists a compact metric space ∞ such that → ∞. Again, this statement involves the construction of the limiting space ∞.
The standard setting for discussing convergence of random objects in probability theory is
that of complete second countable metric spaces (see [
Formalizing the Gromov-Hausdorf space is an interesting task because of the unusual feature that it is a “space” of equivalence classes of spaces (with quotation marks around the first space because of set-theoretic issues). A usable formalization in a mathematics library should retain the following properties: 1. It should interact well with preexisting topological concepts. In other words, if there is a standard notion of compact topological space in the library, then one should be able to talk of the Gromov-Hausdorf distance between such spaces and , and not between new gadgets that would have been defined specifically in view of this formalization. 2. The resulting Gromov-Hausdorf space should also be a topological space in the standard sense of the library. 3. One should be able to define a function mapping a nonempty compact metric space (in the usual sense) to an element of the Gromov-Hausdorf space.
These constraints seem hard to satisfy in simple type theory, where it is not possible to define a function whose arguments are types (the compact space ) and whose images are elements of another type (the Gromov-Hausdorf space). On the other hand, they should not be a problem for a framework based on dependent type theory, with an expressive enough mathematical library. Our formalization is done using the Lean theorem prover, based on a version of the calculus of inductive construction, in the framework of the mathlib library. It satisfies the above requirements. The main results are available in the mathlib ifle topology/metric_space/gromov_hausdorff.lean.
Let us give the form of the interface, i.e., the main definitions and statements, leaving implementation or proof details in ... blocks, before getting to more details. definition GH_space : Type := . . . instance : metric_space GH_space := . . . instance : second_countable_topology GH_space := . . . instance : complete_space GH_space := . . . /−− Mapping a nonempty compact metric space to its equivalence class in ‘GH_space‘. −/ definition to_GH_space (X : Type u) [metric_space X] [compact_space X] [nonempty X] : GH_space := . . . /−− Two nonempty compact spaces have the same image in ‘GH_space‘ if and only if they are isometric. −/ theorem to_GH_space_eq_to_GH_space_iff_isometric {X : Type u} [metric_space X] [compact_space X] [nonempty X] {Y : Type v} [metric_space Y] [compact_space Y] [nonempty Y] : to_GH_space X = to_GH_space Y ↔ nonempty (X ≃ Y) := . . . /−− The Gromov−Hausdorf distance between two spaces ‘X‘ and ‘Y‘ can be realized by isometric embeddings into ‘ ℓ_infty_R‘. −/ theorem GH_dist_eq_Hausdorff_dist (X : Type u) [metric_space X] [compact_space X] [nonempty X] (Y : Type v) [metric_space Y] [compact_space Y] [nonempty Y] : ∃ Φ : X → ℓ_infty_R, ∃ Ψ : Y → ℓ_infty_R, isometry Φ ∧ isometry Ψ ∧ GH_dist X Y = Hausdorff_dist (range Φ ) (range Ψ ) := . . .
In this snippet, GH_space is a type formalizing the Gromov-Hausdorf space, i.e., the space of nonempty compact metric spaces up to isometry. It is endowed with a distance (the GromovHausdorf distance) which turns it into a metric space, in the metric space instance. This metric space turns out to be second-countable and complete. The interface with concrete nonempty compact metric spaces is made through the function to_GH_space, associating to any nonempty compact metric space its equivalence class in the Gromov-Hausdorf space. This definition is used in the form to_GH_space X: the assumptions of the form [...] in this definition are typeclass assumptions on , registering that it is a nonempty compact metric space, and filled in automatically by the system when seeing an expression of the form to_GH_space X. The system raises an error if it can not deduce an instance for these from the context.
The relationship between concrete nonempty compact metric spaces and abstract points in the Gromov-Hausdorf space is illustrated with two theorems: • to_GH_space_eq_to_GH_space_iff_isometric asserts that two spaces have the same image in the Gromov-Hausdorf space if and only if they are isometric; • GH_dist_eq_Hausdorff_dist says that the Gromov-Hausdorf distance between two nonempty compact metric spaces is realized, i.e., one can embed them isometrically in a common metric space so that the Hausdorf distances between their images is exactly their Gromov-Hausdorf distance. The theorem is a little bit stronger, because it says that one can use as a common embedding space the metric space ℓ∞(R) of bounded real sequences, whatever the compact metric spaces and . (See Section 3 for more on this).
Note that the former theorem is an easy consequence of the latter: if and have zero Gromov-Hausdorf distance, then their images under Φ and Ψ given by the second theorem are at zero Hausdorf distance, hence they coincide, and it follows that Ψ − 1 ∘ Φ is an isometry between and .
In the next three sections, we will give more details on three salient points of the formalization.
Until now, we have described the Gromov-Hausdorf space as the “space” of equivalence classes of compact metric spaces up to isometry. There is a problem here: we are quantifying over objects which are not constrained to belong to a given set. This kind of construction is not allowed in set theory, as it leads to Russell-like paradoxes: nonempty compact metric spaces form a class, not a set.
The type theory implemented by Lean makes it possible to circumvent this issue, thanks to the notion of universe level (already dating back to Russell). Informally speaking, any class at universe level becomes an object one can manipulate at level + 1, where range over N. Thus, one can define the type of all nonempty compact metric spaces in universe level , as a well-defined type in universe level + 1. Denote it with . One can then define an equivalence relation ∼ on , saying that two spaces are isometric, and construct a Gromov-Hausdorf space ℋ as / ∼ .
This definition has two drawbacks. First, it depends on the universe level : one does not get one single Gromov-Hausdorf space, but infinitely many of them. This makes it more complicated to discuss the Gromov-Hausdorf distance of two nonempty compact spaces if they come from diferent universes. The second issue is that using universe levels for a construction is often not satisfactory to mathematicians: it means getting out of the standard ZFC framework by adding inaccessible cardinals axioms.
It turns out that the set theoretic issue that there is no set of all compact metric spaces is not a real issue. Indeed, the cardinality of a compact metric space is at most the cardinality of the continuum, which means that the number of non-isometric compact metric spaces is also controlled. For the formalization, this means that we can define one single Gromov-Hausdorf space, in the first universe Type 0 (also called simply Type), the universe in which most natural objects such as N or R live. However, we can not just dismiss the issue as irrelevant, as is done in most textbooks: we have to make a sensible design choice.
We use the following classical proposition.
Proposition 3.1. Consider a compact metric space . There exists an isometric embedding of into the space ℓ∞(R) of bounded real sequences with its distance coming from the sup norm. Proof. Let be a dense sequence in . To a point ∈ , associate the sequence ↦→ (, ). It is easy to check that this defines an isometric embedding of into ℓ∞(R).
This embedding is called the Kuratowski embedding. From this proposition, it follows that all compact metric spaces have isometric representatives as subsets of ℓ∞(R). Therefore, we may define the Gromov-Hausdorf space as the space of all nonempty compact subsets of ℓ∞(R), up to isometry (taking advantage of the built-in quotient construction of Lean). This is an element of Type 0 as announced, as all objects in this definition live in Type 0.
The map to_GH_space, assigning to an arbitrary nonempty compact metric space the corresponding point in GH_space, is then obtained by taking an isometric image of in ℓ∞(R) thanks to Proposition 3.1, and then descending to the quotient GH_space.
Consider two nonempty compact metric spaces and . A key point to show that the GromovHausdorf distance is a distance is to show that there exist a metric space ′ and two isometric copies ′ of and ′ of inside ′ such that the Hausdorf distance ′ (′, ′) is equal to the Gromov-Hausdorf distance (, ) of and . One has always (, ) ≤ ′ (′, ′), and the goal is to construct suitable ′ and ′, ′ such that this inequality becomes an equality.
One can always find a sequence of spaces ′ and isometric embeddings Φ : → ′ and Ψ : → ′ such that ′ (Φ (), Ψ ( )) converges to (, ), by definition of an infimum. The dificulty is that the spaces ′ are unrelated to each other, so making things converge by extracting subsequences has no obvious meaning.
The key idea is to forget completely ′, and only remember its distance. Define a map Θ from the disjoint union ⊔ to ′, equal to Φ on and to Ψ on . Define a function on ( ⊔ )2 by (, ) = (Θ (), Θ ()), where the distance on the right hand side is the distance in ′. This is almost a distance on ⊔ , coinciding with the original distances on and on , except that it does not satisfy in general (, ) = 0 ⇒ = since diferent points in and may be mapped to the same point in ′.
We claim that has a subsequence which converges uniformly to a function ∞ (which is also almost a distance in the previous sense). Define a space to be the quotient of ⊔ identifying two points and when ∞(, ) = 0. This is a metric space, in which and embed isometrically and realizing the Gromov-Hausdorf distance by construction.
It remains to check the claim. This is a consequence of the classical Arzela-Ascoli theorem: Theorem 4.1. Let : → be a sequence of bounded continuous functions on a compact space , with range included in a compact subset of the metric space . Assume that the functions are equicontinuous: for every ∈ and every > 0, there exists a neighborhood of such that for every ∈ N and every ∈ , one has ((), ()) ≤ . Then admits a uniformly converging subsequence.
Indeed, one checks readily that the family of functions on the compact space ( ⊔ )2 is equicontinuous (it is even uniformly Lipschitz-continuous). Unfortunately,the ArzelaAscoli theorem was not available in mathlib at the time of the formalization of the GromovHausdorf space (and neither was the notion of uniform convergence!). An important part of this formalization was therefore devoted to all these prerequisites, including the definition and study of the Banach space of bounded continuous functions on a topological space.
It is worth pointing out that, since then, these results have been put to good use in completely diferent directions in mathlib (for instance to formalize the Stone-Weierstrass theorem, asserting that an algebra of continuous functions separating points on a compact space is dense in the space of continuous functions). This is an important point of the formalization of fairly specialized concepts such as the Gromov-Hausdorf space: it is a way to notice general-purpose gaps in the library and to fill them. The mathlib philosophy is that these gaps should not be iflled just in the minimal way needed to prove the target theorem, but in the maximal possible generality to make it suitable for further uses in diferent directions. For instance, during the formalization of the Gromov-Hausdorf distance, the notion of uniform convergence has been defined in the maximal generality of uniform spaces, even if we only needed the case of metric spaces for this specific application.
To prove the completeness of the Gromov-Hausdorf space, we will need to glue metric spaces along isometric subspaces, as follows. Assume that and are two metric spaces, and that another metric space admits two isometric embeddings Φ : → and Ψ : → . Then one can form a new space by identifying the two subsets in and , and this new space is naturally a metric space, containing isometric copies of both and .
Let us now explain why the Gromov-Hausdorf space is complete. It is enough to show that a sequence of compact spaces satisfying (, +1) ≤ 2− converges. The dificulty is that we need to construct in some way the limiting metric space. The idea is to embed simultaneously all the in a common metric space ∞, with controlled mutual Hausdorf distances, and use the fact that the space of compact nonempty subsets of ∞, with the Hausdorf distance, is complete, to get the desired limit as a subset of ∞.
There exists for each a metric space containing isometric copies of − 1 and of which are at Hausdorf distance ≤ 2− , by Section 4. Let us now define inductively a sequence of metric spaces containing isometric copies of 0, . . . , , as follows.
1. Start with 0 = 0. 2. Assume is defined. It contains an isometric copy of . So does +1. Therefore, we may glue and +1 along their respective copies of , to obtain the new space +1. It contains a copy of +1 (the one contained in +1) and copies of 0, . . . , (the ones contained in ).
Define a suitable limit ∞ of the increasing family (formally, an inductive limit). It is a metric space, containing for each a copy ′ of . By construction, the Hausdorf distance ∞ (′, ′+1) is ≤ 2− . Since, on a given complete metric space, the space of its nonempty compact subsets is a complete space for the Hausdorf distance, it follows that ′ converges, to a compact subset ∞′ of ∞. Then, in the Gromov-Hausdorf space, converges to the class of ∞′.
There is an interesting feature in the formalization of this proof, in the inductive definition of the space , highlighting several shortcomings of Lean 3. One should define simultaneously the space , but also a metric space structure on it, and an isometric embedding of in (which only makes sense given the metric space structure). And the next step of the construction will take advantage of all these data to proceed. The most natural formalization would be by several mutually inductive definitions, but Lean 3 has weaknesses in this area. Instead, we used one single structure containing all these data, and one big induction to define the structure at step + 1 from the structure at step . Another issue is that the Lean 3 equation compiler generates a definition in terms of bounded recursion which is not easy to use. We use instead a direct definition in terms of the recursor for natural numbers. Here is the full inductive definition we use. variables (X : N → Type) [∀ n, metric_space (X n)] [∀ n, compact_space (X n)] [∀ n, nonempty (X n)] /−− Auxiliary structure used to glue metric spaces below, recording an isometric embedding of a type ‘A‘ in another metric space. −/ structure aux_gluing_struct (A : Type) [metric_space A] : Type 1 := (space : Type) (metric : metric_space space) (embed : A → space) (isom : isometry embed) /−− Auxiliary sequence of metric spaces, containing copies of ‘X 0‘, . . ., ‘X n‘, where each ‘X i‘ is glued to ‘X (i+1)‘ in an optimal way. The space at step ‘n+1‘ is obtained from the space at step ‘n‘ by adding ‘X (n+1)‘, glued in an optimal way to the ‘X n‘ already sitting there. −/ def aux_gluing (n : N) : aux_gluing_struct (X n) := nat.rec_on n { space := X 0, metric := by apply_instance, embed := id, isom := λ x y, rfl } (λ n Z, by letI : metric_space Z.space := Z.metric; exact { space := glue_space Z.isom (isometry_optimal_GH_injl (X n) (X (n+1))), metric := by apply_instance, embed := (to_glue_r Z.isom (isometry_optimal_GH_injl (X n) (X (n+1)))) ∘ (optimal_GH_injr (X n) (X (n+1))), isom := (to_glue_r_isometry _ _).comp (isometry_optimal_GH_injr (X n) (X (n+1))) })
We start from a context in which a sequence of nonempty compact metric spaces is given, which we want to glue together. The structure aux_gluing_struct A records a metric space containing an isometric copy of a metric space . The definition aux_gluing n constructs inductively over a metric space containing an isometric copy of (and also of all the previous ones, by design, but we only register the last one for the inductive construction). For = 0, it is just 0. At the ( + 1)-th step, it glues two spaces containing an isometric copy of along as explained in Section 4: on the one hand the space constructed at the previous step; on the other hand a space in which the Gromov-Hausdorf distance between and +1 is realized.
The reader may note the line letI : metric_space Z.space := Z.metric at the beginning of the inductive step in the construction. By induction, the space Z.space constructed at step has a metric space structure, called Z.metric. However, this metric space structure is not yet available to typeclass inference: there is a caching mechanism underneath (which is very important performancewise as typeclass inference is quite costly), so new instances need to be declared explicitly just like here. Once this preliminary incantation has been done, the system knows about the metric space structure on Z.space and is happy with the statement that a map to Z.space is an isometry, for instance. This is needed for the next step of the construction to go through.
Once this inductive definition has been set up properly (together with enough properties of the gluing of metric spaces, and of inductive limits of metric spaces), the rest can be formalized without any specific dificulty.