Constructs a smooth positive-definite metric on (-1,1)^2 for which no neighborhood of the origin admits a smooth isometric immersion into ℝ3. This answers the unrestricted smooth local isometric realization problem for surfaces negatively, even after shrinking the neighborhood. (Lean)
Manuscript
A Smooth Metric with No Local Isometric Immersion into Three-Space
September 24, 2026 · source · Lean formalization available · cite as \cite{OAI:A-Smooth-Metric-with-No-Local-Isometric-Immersion-into-Three-Space-September-24-2026}
We construct a smooth positive-definite Riemannian metric on (-1,1)^2 that agrees with the Euclidean metric to every order at the origin, yet no neighborhood of the origin admits a smooth isometric immersion into Euclidean three-space. This gives a negative answer to the unrestricted smooth local isometric realization problem for surfaces.
Result 334 · Differential geometry. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.
Source: https://github.com/openai/math/blob/main/CONTENTS.md