Tingley's problem: does every surjective isometry between unit spheres of Banach spaces extend to a linear isometry?
For a real normed space let be its unit sphere with the inherited metric. Mazur and Ulam (1932) proved that surjective isometries between real normed spaces are affine, but a unit sphere has empty interior, so this does not apply. Tingley (1987) asked whether every surjective isometry between unit spheres of real Banach spaces extends to a real-linear isometry of onto . Positive answers were known for many classical spaces (, , von Neumann algebras and their preduals, unital -algebras) and for every two-dimensional space (Banakh 2022), but not in general, even in finite dimension. Does every surjective isometry between the unit spheres of two real Banach spaces extend to a surjective real-linear isometry?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Functional analysis; geometry of Banach spaces
- Posed by
- Daryl Tingley, Isometries of the unit sphere, Geometriae Dedicata 22 (1987)
- Year posed
- 1987
- Years open
- 39y
- Solved
- 2026-09-23
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 38 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: if are nonzero real Banach spaces and is a surjective isometry, then , is a surjective real-linear isometry, the unique linear extension of . No separability, reflexivity, smoothness, strict convexity or finite-dimensionality is assumed. For complex spaces only real linearity is concluded. The proof uses a maximal-defect argument, common supports and Darbo's fixed-point theorem. Incomplete normed spaces are not treated.
What the AI did
The release README says the results were produced by an unreleased internal OpenAI model with a fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result, and that some outputs build on earlier model results. This result is not among the README's exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region). The manuscript is authored 'OpenAI' and names no human author.
Verification
No independent mathematician has checked this yet. Checked here: Theorem 1.1 was read against Tingley's question as the paper states it from Tingley (1987); it claims that for nonzero real Banach spaces the radial map is a surjective real-linear isometry and the unique linear extension. The proof was not refereed. lean/formalization.yaml lists a main result (comparator TingleySphereIsometry, declaration OAI.Tingley.tingley_sphere_isometry_full, file OAI/Analysis/SphereIsometry/Extension.lean). ComparatorChallenges/TingleySphereIsometry.lean was read here: for complete, nontrivial real normed spaces of any size and a surjective isometry between unit spheres, it asserts a linear isometric equivalence agreeing with on the sphere, given by the radial formula, and unique among real-linear maps extending . This states the headline claim. Not rebuilt here.