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 'Asymptotic midpoint uniform convexity and unbounded diamond distortion in a reflexive tree space'. We construct a separable reflexive real Banach space whose given norm is asymptotically midpoint uniformly convex but which admits no asymptotically uniformly convex equivalent norm. Its averaged midpoint modulus is at least \sqrt{1+t^2/12}-1, and the countably branching diamond of depth k has distortion at least \sqrt{1+k/12} in this space. This gives a negative answer to the reflexive diamond converse for asymptotic uniform convexifiability.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 331). The Lean development was not rebuilt locally.