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 'Projection moments, positive cap domination, and Riesz estimates on the sphere'. We prove moment estimates for exact random projections of finite measures whose mass is controlled on Euclidean balls, and derive positive domination by countable sums of spherical cap measures. For learners with M=o(d^2) bits of memory, these estimates give three proofs that uniform-sphere average success at least 2/3 at angular accuracy 0\lt \epsilon\le1/10 requires \Omega(d\log(1/\epsilon)) noiseless Gaussian observations. The three proofs keep their different stopping and accuracy costs explicit.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 140). The Lean development was not rebuilt locally.