Subpolynomial dimension reduction in L_p

1 paperLean

For every fixed \(1\lt p\lt \infty\) and distortion D > 1, every n-point subset of real L_p embeds into \(\ell_p^d\) with distortion at most D and dimension \(d=n^{o(1)}\), answering Naor's sublinear-dimension question for p ≠ 2. In contrast, exact embeddings require worst-case dimension \(\Theta(n^2)\) when p ≠ 2.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

Subpolynomial dimension reduction in Lp

OpenAI · September 23, 2026

For every fixed \(1\lt p\lt \infty\) and D > 1, every n-point subset of a real L_p space embeds into \(\ell_p^d\) with distortion at most D and subpolynomial dimension \(d=n^{o(1)}\). The target has the same exponent p, and the embedding need not be linear.

Read PDF Download Source

Cite

@misc{OAI:Subpolynomial-dimension-reduction-in-Lp-September-23-2026,
  author = {{OpenAI}},
  title = {{Subpolynomial dimension reduction in $L_p$}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Subpolynomial-dimension-reduction-in-Lp-September-23-2026/paper.pdf}{OAI:Subpolynomial-dimension-reduction-in-Lp-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

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

Subpolynomial dimension reduction in \(L_p\)

Scope

For \(p>1\), \(p\ne2\), the formalization bounds the least dimension needed to embed every \(n\)-point subset of real \(L_p\) with distortion \(D\). For each fixed \(D>1\), there is a constant \(C=C(p,D)\) such that this dimension lies between \(\log n/\log(1+2D)\) and \(\exp(C(\log n)^{\gamma(p)})\) for every \(n\ge2\), where \(\gamma(p)=2-p\) for \(p<2\) and \(1-2/p\) for \(p>2\). At distortion \(1\) and \(n\ge9\), it lies between \(\lfloor(n-1)/4\rfloor^2\) and \(\binom n2\). The least dimension is attained, and its logarithm divided by \(\log n\) tends to \(0\) for \(D>1\) and to \(2\) for \(D=1\).

Comparator links

Result	Comparator statement
Dimension reduction in \(L_p\)	SubpolynomialLp.lean

Scope note on GitHub →