Lean formalization in OpenAI math repository (Result 322)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'A positive solution to Tingley's problem'. Every surjective isometry between the unit spheres of real Banach spaces extends uniquely to a surjective real-linear isometry, giving an affirmative solution to Tingley's problem. If distances between different radii are not preserved, we realize the positive maximal defect in a possibly enlarged pair of Banach spaces. We then align extremal chords using common supports and Darbo's fixed-point theorem and obtain a contradiction from support and convexity estimates.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 322). The Lean development was not rebuilt locally.