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 'Midpoint convexity from bounded tree potentials and path costs'. Four real Banach spaces defined by bounded tree potentials satisfy the averaged asymptotic midpoint bound \widehat\delta(t)\ge\sqrt{1+t^2/4}-1 for 0\lt t\lt 1, while none admits an asymptotically uniformly convex (AUC) renorming. On finite-height trees, the globally constrained norm equals the least additive cost of a Hilbert vector and root paths. The quadratic path and segment-start outer Hilbert sums are reflexive and asymptotically midpoint uniformly convex, and admit no equivalent AUC norm.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 331). The Lean development was not rebuilt locally.