Oct 6, 2026
Lean formalization in OpenAI math repository (Result 140)
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 'Memory and precision in noiseless Gaussian regression'. For every fixed A > 0, a learner that retains at most Ad^2 bits between fresh exact Gaussian linear measurements needs \Omega_A(d\log(1/\epsilon)) measurements to estimate a uniformly random unit vector to angular error at most ϵ, for any 0\lt \epsilon\le 1/10, with probability at least 2/3. The constant is absolute for o(d^2) memory.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 140). The Lean development was not rebuilt locally.