Lean formalization in OpenAI math repository (Result 139)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Subpolynomial query complexity for well-conditioned log-concave sampling'. For every fixed ε > 0, we give a sampling algorithm using at most C_\varepsilon d^\varepsilon exact first-order queries on every execution for C2 potentials on ℝd with a known minimizer and Hessian between Id and 2I_d. The output has total-variation distance at most 1/10 from the target Gibbs law. Computation between queries is unrestricted. We also prove an \Omega(\log d) query lower bound for arbitrary randomized adaptive algorithms, determining the optimal dimension exponent to be zero.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 139). The Lean development was not rebuilt locally.