# Tingley’s sphere-isometry problem

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A positive solution to Tingley's problem](../../preprints/A-positive-solution-to-Tingleys-problem-September-23-2026/paper.pdf)

## Scope

Tingley's problem asks whether a surjective isometry between the unit spheres of Banach spaces extends to a linear isometry of the spaces. The formalized result gives a unique surjective real-linear isometric extension for arbitrary nonzero real Banach spaces, with no finite-dimensionality, separability, reflexivity, or convexity assumptions. For complex spaces viewed as real spaces, the conclusion is real linearity rather than complex linearity.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Tingley's sphere-isometry extension | [TingleySphereIsometry.lean](../ComparatorChallenges/TingleySphereIsometry.lean) |