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 two recursive potentials'. We study tree norms computed by two least nonnegative fields whose difference is the vector. For Euclidean child aggregation, two root-sum spaces have an averaged asymptotic midpoint modulus of at least t^3/128 for 0\lt t\lt 1, including a reflexive joining-root space. A reflexive construction with a fixed zero root also satisfies a homogeneous cubic estimate. These spaces admit no equivalent asymptotically uniformly convex norm. We also obtain sixth-power and cubic estimates when the aggregation exponent depends on the height of a finite component.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 331). The Lean development was not rebuilt locally.