Prove TingleySphereIsometry (openai/math family 322: Tingley's sphere-isometry problem) in Lean 4 with…
Prove TingleySphereIsometry (openai/math family 322: Tingley's sphere-isometry problem) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 322 of the release, Tingley's sphere-isometry problem (Functional analysis). The family…
The task
Context: this statement belongs to family 322 of the release, *Tingley's sphere-isometry problem* (Functional analysis). The family as a whole: Resolves Tingley's problem: every surjective isometry between the unit spheres of nonzero real Banach spaces extends uniquely to a surjective real-linear isometry of the…
Part of raising-heart/openai-math.