Lean formalization in OpenAI math repository (Result 360)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Global Support and Convex Injectivity Domains under Weak MTW'. We prove that weak Ma–Trudinger–Wang curvature on a smooth, connected, compact Riemannian manifold of dimension at least two without boundary implies convexity of every tangent injectivity domain, resolving Villani's conjecture in this setting. Conjugate cut points are allowed. More generally, every ordinary subgradient of a squared-distance cost potential is a minimizing velocity with a global supporting mountain. No density hypothesis is used.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 360). The Lean development was not rebuilt locally.