Lean formalization in OpenAI math repository (Result 140)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Replacing Gaussian observations in memory-constrained inference'. Replacing the Gaussian rows used to select a finite message by independent rows increases the remaining conditional information by at most Cd, for a uniform spherical signal, message entropy at most d2, and the specified row dimensions proportional to d. As an application, we prove that learners with M=o(d^2) persistent bits need T=\Omega(d\log(1/\epsilon)) exact observations to attain uniform-sphere angular success at least 3/5, for 0\lt \epsilon\le1/10 and a deterministic finite horizon.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 140). The Lean development was not rebuilt locally.