∑math20

Convex and metric geometry · Result 098

Compact counterexamples to bi-Lipschitz dimension reduction

1 paperLean

Every infinite-dimensional real Banach space contains a compact doubling set that admits no bi-Lipschitz embedding into any finite-dimensional normed space. The doubling constant is universal. This answers the Lang–Plaut problem negatively, even for compact subsets of Hilbert space.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embedding

A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embedding

OpenAI · September 25, 2026

Every infinite-dimensional real Banach space contains a compact doubling subset that admits no bi-Lipschitz embedding into any finite-dimensional real normed space. The doubling constant has a universal bound, independent of the ambient Banach space. This answers the Lang–Plaut problem negatively, even for compact subsets of Hilbert space.

Read PDF Download Source

Cite
@misc{OAI:A-doubling-Hilbert-subset-with-no-finite-dimensional-bi-Lipschitz-embedding-September-25-2026,
  author = {{OpenAI}},
  title = {{A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embedding}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-doubling-Hilbert-subset-with-no-finite-dimensional-bi-Lipschitz-embedding-September-25-2026/main.pdf}{OAI:A-doubling-Hilbert-subset-with-no-finite-dimensional-bi-Lipschitz-embedding-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalized result gives a doubling subset of real \(\ell_2\), with doubling constant at most \(76800\), that admits no bi-Lipschitz embedding into any finite-dimensional Euclidean space at any finite distortion. A companion gives one universal doubling constant such that every infinite-dimensional real Banach space contains a compact doubling subset with no bi-Lipschitz embedding into any finite-dimensional normed space.

Comparator links

ResultComparator statement
Doubling Hilbert subset without finite-dimensional embeddingDoublingHilbert.lean
Compact counterexamples in infinite-dimensional Banach spacesCompactBanach.lean

Scope note on GitHub →