Lean formalization in OpenAI math repository (Result 331)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Exact asymptotic moduli in a Daugavet subspace of L1'. For an infinite-dimensional real subspace of L1 whose unit ball is totally bounded in measure and whose norm has the Daugavet property, we compute the averaged midpoint and one-sided asymptotic moduli at every unit center. They are \max\{t/2,t-1\} and \max\{0,t-2\}, respectively. The same weak-neighborhood geometry excludes every equivalent asymptotically uniformly convex norm. A quantitative realization of the Kadets–Werner construction supplies a space with both hypotheses.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 331). The Lean development was not rebuilt locally.