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 'Subsphere methods for memory–sample lower bounds in noiseless Gaussian regression'. Let a finite-state streaming learner estimate a uniformly random unit vector from independent exact Gaussian linear measurements. We prove that o(d^2) bits of persistent memory and angular success probability at least 2/3 require at least 2^{-16}d\log_2(1/\epsilon) samples for all sufficiently large d, uniformly for 0\lt \epsilon\le1/10. The proof conditions each batch on its observed projection and controls the resulting random residual subsphere.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 140). The Lean development was not rebuilt locally.