The Lang–Plaut problem

The Lang–Plaut problem asks whether every doubling subset of Hilbert space admits a bi-Lipschitz embedding into some finite-dimensional Euclidean space. A manuscript in OpenAI's public mathematics collection (github.com/openai/math), dated 25 September 2026, claims a negative answer: a doubling subset of Hilbert space with no such embedding, and, in every infinite-dimensional real Banach space, a compact doubling subset with no bi-Lipschitz embedding into any finite-dimensional normed space. The collection includes a Lean formalization of both statements. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

• As recounted in the introduction of the manuscript:
  • The question is Lang and Plaut's Question 2.4, restated by Naor and Neiman; Gupta, Krauthgamer and Lee formulated it independently in the context of algorithmic dimension reduction. Assouad's theorem gives embeddings after snowflaking the metric, and Naor and Neiman bounded the target dimension in terms of the doubling constant alone for exponents close to 1.
  • For ambient exponents p > 2, Lafforgue and Naor constructed doubling subsets of L_p with no bi-Lipschitz embedding into any finite-dimensional Euclidean space; Bartal, Gottlieb and Neiman independently obtained dimension-reduction obstructions in ℓ_p, and Baudier, Świȩcicki and Swift gave an elementary proof for ℓ_q, q > 2. These do not settle the Hilbert case.
  • Schioppa announced a negative answer in 2017 (arXiv:1703.10265) and withdrew the preprint after reporting a possible issue with its duality argument.

The original results

• Claim. Theorem 1 of A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embedding states that there is a fixed subset of real ℓ₂, with its induced distance, whose doubling constant is at most 76,800 and which admits no bi-Lipschitz embedding into R^k for any k and any finite distortion. The manuscript also realizes the same metric space isometrically in L_p[0,1] for every 1 ≤ p < ∞, and constructs in every infinite-dimensional real Banach space a compact doubling subset, with one universal doubling constant, that admits no bi-Lipschitz embedding into any finite-dimensional normed space.
• Method, as described: the set is built over the plane from orthogonal displacements at rapidly separated scales, assigned by periodic colourings of horizontal and vertical strips. A putative embedding is restricted to "sheets" over the plane; an extremal choice of the squared norms of the two derivative columns forces small variation of relative offsets along lines of each colour, and the crossings of rows and columns of different colours then contradict the bound on the number of well-separated points in a ball of R^k.
• Source. The manuscript A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embedding at commit 1581d4c.
• Formalization, as described by the repository. The scope note states that the formalization gives a doubling subset of real ℓ₂ with doubling constant at most 76,800 and no bi-Lipschitz embedding into any finite-dimensional Euclidean space at any finite distortion, and, as a companion, one universal doubling constant for which every infinite-dimensional real Banach space contains a compact doubling subset with no bi-Lipschitz embedding into any finite-dimensional normed space. The Comparator statements are DoublingHilbert.lean and CompactBanach.lean.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 20 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026)	Review (fidelity of the formal statements)	Rates this family "full", with no issue noted, and records sandboxed Comparator passes for DoublingHilbert and CompactBanach.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-10	cert-machine, openai/math lane K	Verification (two kernels)	Records that Lean's default kernel and the nanoda kernel accept the DoublingHilbert solution (237 s, run 38019899278) and the CompactBanach solution (232 s, run 38017370880). The project reports two-kernel certification of 398 of 416 challenges of the collection.	Repository.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list DoublingHilbert or CompactBanach, so the challenges were accepted by con-leche and by Lean's official kernel.	Development journal.

Notes

• The results for exponents p > 2 and the snowflake embeddings are due to the authors named in the Background section, as recounted by the manuscript.
• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.