Oct 6, 2026
Lean formalization in OpenAI math repository (Result 098)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embedding'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 098). The Lean development was not rebuilt locally.