The sphere knows all?
An AI preprint claims a solution to Tingley’s problem, with a full Lean proof
Covers result 322 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
3:42. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
In a normed plane the unit circle need not be round. With the largest coordinate as the norm, it is a square; with the sum of absolute values, a diamond. Distances are measured straight through the plane. Now take two such spaces and a map from one unit sphere onto the other that keeps every distance. In 1987 Daryl Tingley asked whether such a map must always come from a linear isometry of the whole spaces.
For whole spaces, the theorem of Mazur and Ulam from 1932 says yes, up to a shift, but a sphere has no inside, so neither that theorem nor its extension to solid shapes reaches it. Special cases followed: polyhedral spaces in finite dimensions, by Kadets and Martín in 2012; operator algebras; and every 2-dimensional space, by Banakh in 2022. Papers from 2023 to August 2026 still called it open; the earlier ones said so for dimension 3 and higher.
Result 322 is one OpenAI paper, 12 pages, dated September 23 and made public October 6, 2026. It claims the full answer: for any nonzero real Banach spaces, every surjective isometry between their unit spheres extends, by stretching each ray, to a surjective real-linear isometry, and to only one. Any dimension, even infinite; no separability, smoothness or strict convexity needed.
What it doesn’t claim
Not claimed: complex linearity. For complex spaces the extension is only real-linear, and complex conjugation shows that is the best possible. Not claimed either: maps that are not onto. Our computer finds one that keeps every sphere distance, but sends opposite points to points that are not opposite, so no linear map extends it.
Where it stands
- Posted as a preprint
- OpenAI, 12 pages, dated September 23, 2026
- Peer reviewed
- Not yet
- Formalized in Lean
- The full theorem (docs)
Last checked October 19, 2026. The paper is unrefereed and unchanged since release. Unusually, the Lean formalization states the full theorem, matching the paper, with only the standard axioms: 67 files and about 9,000 lines, not run by us. Two outside projects re-ran the check and it was accepted, and one of them judged the formal statement faithful to the claim. No specialist has published an assessment; one specialist’s site posted a ChatGPT-drafted exposition that reports no error, but says it is not an independent solution and not a human proof review. OSVerify has not reviewed it.
How the proof goes
- One number: the worst error. Stretching rays is the only candidate, and it already keeps distances between points at the same radius. So the whole problem is one number: the worst error in distances between different radii. The paper calls it M and supposes it is positive. By enlarging both spaces with an ultrapower, it makes that worst error actually attained.
- A return map, and chords that can’t exist. Next, a return map on directions: shoot a ray to the sphere, map it across, shoot back, and pull it home. Darbo’s fixed-point theorem, proved from scratch in the appendix, gives a direction that returns to itself, and with it two perfectly aligned chords. Then convexity of the norm, with the maximality of M, shows those chords cannot exist. So M is zero, and the Mazur–Ulam step makes the map linear. Our computer checks small cases: on a diamond with just 4 points, 24 shuffles keep every distance and only 8 are linear, but add the edge midpoints and every shuffle that keeps distances is linear.
The numbers in the video
- Ours: on the diamond (the unit circle of the sum norm) with its 4 corners, 24 shuffles keep every distance and only 8 are linear; with the 4 edge midpoints added, all 8 distance-keeping shuffles are linear.
- Ours: with the max norm, f(x₁, x₂) = (x₁, x₂, 1) keeps every sphere distance but is not onto, and f(−x) ≠ −f(x), so no linear map extends it.
- Lean: 67 files and 9,273 lines in the proof’s import closure (counted by us; not run by us).
Read the source
- A positive solution to Tingley’s problem (PDF), 12 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 322.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
In a normed plane the unit circle need not be round. With the largest coordinate as the norm, it is a square; with the sum of absolute values, a diamond. Distances are measured straight through the plane. Now take two such spaces and a map from one unit sphere onto the other that keeps every distance. In 1987 Daryl Tingley asked whether such a map must always come from a linear isometry of the whole spaces. For whole spaces, the theorem of Mazur and Ulam from 1932 says yes, up to a shift, but a sphere has no inside, so neither that theorem nor its extension to solid shapes reaches it. Special cases followed: polyhedral spaces in finite dimensions, by Kadets and Martín in 2012; operator algebras; and every 2-dimensional space, by Banakh in 2022. Papers from 2023 to August 2026 still called it open; the earlier ones said so for dimension 3 and higher.
1:00The claim
Result 322 is one OpenAI paper, 12 pages, dated September 23 and made public October 6, 2026. It claims the full answer: for any nonzero real Banach spaces, every surjective isometry between their unit spheres extends, by stretching each ray, to a surjective real-linear isometry, and to only one. Any dimension, even infinite; no separability, smoothness or strict convexity needed. Not claimed: complex linearity. For complex spaces the extension is only real-linear, and complex conjugation shows that is the best possible. Not claimed either: maps that are not onto. Our computer finds one that keeps every sphere distance, but sends opposite points to points that are not opposite, so no linear map extends it.
1:49How the proof goes
Stretching rays is the only candidate, and it already keeps distances between points at the same radius. So the whole problem is one number: the worst error in distances between different radii. The paper calls it M and supposes it is positive. By enlarging both spaces with an ultrapower, it makes that worst error actually attained. Next, a return map on directions: shoot a ray to the sphere, map it across, shoot back, and pull it home. Darbo’s fixed-point theorem, proved from scratch in the appendix, gives a direction that returns to itself, and with it two perfectly aligned chords. Then convexity of the norm, with the maximality of M, shows those chords cannot exist. So M is zero, and the Mazur–Ulam step makes the map linear. Our computer checks small cases: on a diamond with just 4 points, 24 shuffles keep every distance and only 8 are linear, but add the edge midpoints and every shuffle that keeps distances is linear.
2:50Where it stands
The paper is unrefereed and unchanged since release. Unusually, the Lean formalization states the full theorem, matching the paper, with only the standard axioms: 67 files and about 9,000 lines, not run by us. Two outside projects re-ran the check and it was accepted, and one of them judged the formal statement faithful to the claim. No specialist has published an assessment; one specialist’s site posted a ChatGPT-drafted exposition that reports no error, but says it is not an independent solution and not a human proof review. If it holds, the distances on a unit sphere alone determine a real Banach space up to a linear isometry, in every dimension, and Tingley’s question has the answer yes.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.