Oct 6, 2026
Lean formalization in OpenAI math repository (Result 094)
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 'Subpolynomial dimension reduction in L_p'. For every fixed 1\lt p\lt \infty and D > 1, every n-point subset of a real Lp 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 094). The Lean development was not rebuilt locally.