Tingley's problem
From OpenAI Aftermath
Tingley's problem asks whether every surjective isometry between the unit spheres of two real Banach spaces extends to a real-linear isometry between the whole spaces. A manuscript in OpenAI's public mathematics collection (github.com/openai/math) claims a positive solution for all nonzero real Banach spaces.
Background
- As recounted in the introduction of the manuscript:
- Tingley posed the problem in 1987 and showed that surjective isometries between the unit spheres of finite-dimensional Banach spaces preserve antipodal points. Mazur and Ulam proved that surjective isometries between real normed spaces are affine, and Mankiewicz extended isometries between convex sets with nonempty interior; a unit sphere has empty interior, so these results do not apply directly.
- Positive results for concrete spaces include Wang's for the spheres of complex C0-spaces and Ding's for ℓp(Γ)-type spaces. Cheng and Dong formulated the Mazur–Ulam property, an extension for every surjective sphere isometry into an arbitrary real Banach space, and Tan proved it for real Lp(μ) with 1 < p < ∞, p ≠ 2.
- In the operator-algebra programme, Fernández-Polo and Peralta proved extension theorems between complex von Neumann algebras, Mori between their preduals, and Mori and Ozawa the Mazur–Ulam property for unital complex C*-algebras and real von Neumann algebras. In finite dimensions, Banakh proved the Mazur–Ulam property for every two-dimensional real Banach space.
The original result
- Claim. Theorem 1.1 of A positive solution to Tingley's problem states that if X and Y are nonzero real Banach spaces and f : SX → SY is a surjective isometry between their unit spheres, then the radial map T(0) = 0, T(x) = ‖x‖ f(x/‖x‖) is a surjective real-linear isometry, and it is the unique linear extension of f. The spaces may have any dimension and need not be separable, reflexive, smooth or strictly convex; for complex spaces regarded as real spaces the conclusion is real linearity.
- Method, as described: a hypothetical positive defect in preserving distances between two radius levels is made to attain its maximum in a possibly enlarged pair of Banach spaces. Extremality propagates through common supporting functionals to an invariant closed convex set of directions, on which a return map contracts the Kuratowski measure of noncompactness, so that Darbo's fixed-point theorem gives two aligned extremal chords; support and convexity estimates then rule them out.
- Source (openai/math repository, commit
7ef5c0c): A positive solution to Tingley's problem, dated 23 September 2026. - Formalization, as described by the repository. The scope note lean/docs/322.md states that the formalized result gives the unique surjective real-linear isometric extension for arbitrary nonzero real Banach spaces, with no finite-dimensionality, separability, reflexivity or convexity assumption, and links the comparator statement TingleySphereIsometry.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 28 October 2026) |
|---|---|---|---|---|
| 2026-10-06 | Tingley's sphere-isometry extension, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Outlines the manuscript's defect attainment, the return-map estimate for the measure of noncompactness and the final chord contradiction. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification. |
| 2026-10-08 | Formal Conjectures pull request 6988 by the GitHub user anxkhn, Add Tingley's sphere-isometry theorem, resolving issue 6983 | Formalization (Lean statement) | Adds a Lean statement of the extension assertion of Theorem 1.1 to the Formal Conjectures catalogue, using existing Mathlib types, without a proof; it notes that the radial formula and uniqueness follow from linearity and agreement on the sphere. | Open pull request as of 28 October 2026, approved by a reviewer on 10 October 2026. The description states that it was prepared with AI assistance in OpenCode. |
| 2026-10-09 | Tingley's problem, a course on Open Mathematics Courses (kokunoyumeto/open-math-courses-public) | Reading (exposition) | Four lessons with proofs, examples and solved exercises: the Mazur–Ulam theorem, a hypothetical positive defect made to attain its maximum in an ultrapower, aligned extremal chords as a fixed point of a return map by Darbo's theorem, proved from Schauder's and Brouwer's, and their exclusion by support, secant and convexity estimates. | The course states that it was written and self-checked by Claude Opus 5.5 of Anthropic, that self-checking is not independent mathematical review, and that independent review is not complete. |
| 2026-10-14 | A reader's reconstruction of the chord argument for Tingley's problem, expository note, version 1, on the website Exact Mathematics with AI | Reading (exposition) | A 21-page note that reorganizes the argument and simplifies some steps, treating in detail the construction of the convex invariant set by successive convex enlargement and the explicit support estimates before the comparison of the two chord coordinates. It attributes the proof to the manuscript and states that it is not an independent solution. | Published 14 October 2026, with publication responsibility by Ryotaro Tanaka. The note states that it was drafted and revised using ChatGPT and does not claim independent human proof review or Lean formalization. |
| 2026-10-14 | K. Kudaybergenov, M. Ibragimov and A. Arziev, arXiv:2610.19626 (v1), titled Isometries of unit spheres of SFS-spaces and a geometric approach to Tingley's problem | Parallel (special case) | Shows that surjective isometries between the unit spheres of facially symmetric spaces preserve symmetric faces, orthogonality, geometric tripotents and Peirce structure, and as an application gives a positive solution of Tingley's problem for finite-dimensional real neutral strongly facially symmetric spaces with the joint Peirce property, with an extension result for a wider class. | arXiv preprint, version 1; it does not cite the manuscript. |
| 2026-10-19 | AI Proved What?, episode 322 The sphere knows all?, remade version of 23 October 2026 | Reading (exposition) | Video explainer of the claim that for any nonzero real Banach spaces, of any dimension and without separability, smoothness or strict convexity, every surjective isometry between their unit spheres extends uniquely, by stretching each ray, to a surjective real-linear isometry. The episode states that complex linearity is not claimed, complex conjugation showing that real linearity is best possible, and that maps which are not onto are not covered, giving its own example of a sphere-distance-preserving map with no linear extension. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 19 October 2026: posted as a preprint: OpenAI, 12 pages, dated September 23, 2026; under expert review: not yet; peer reviewed: not yet; formalized in Lean: the full theorem. |
| 2026-10-23 | C.-W. Leung, C.-K. Ng and N.-C. Wong, arXiv:2610.32029 (v1), titled Reconstructing the Jordan structure of C*-algebras from the metric on positive unit spheres | Related (cites the manuscript) | Shows that the diametral relation on the positive unit spheres of unital C*-algebras determines their Jordan structure when the algebra has no two-dimensional irreducible representation. It cites the manuscript as a recent preprint resolving Tingley's problem for all real Banach spaces. | arXiv preprint, version 1. |
Notes
- The background summarizes the manuscript's own account of earlier work.
- J. Nakamura and R. Tanaka, arXiv:2609.31096, posted on 25 September 2026, before the public release of the collection on 6 October 2026, prove that finite-dimensional real normed spaces with isometric unit spheres are linearly isometric, answering a question of Kadets and Martín in finite dimensions; their abstract states that it does not assert the linear extension of a prescribed sphere isometry. It is listed here as related work, not as a follow-up.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
