Oct 6, 2026
Lean formalization in OpenAI math repository (Result 360)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Uniform Bi-Hölder Transport from Weak MTW'. We prove that the weak Ma–Trudinger–Wang condition on a fixed smooth connected compact boundaryless Riemannian manifold of dimension at least two implies a common Hölder estimate for optimal transport maps and their inverses over the entire class of probability densities with fixed positive upper and lower bounds. The maps have homeomorphic representatives, conjugate cut points are allowed, and no density regularity is assumed.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 360). The Lean development was not rebuilt locally.