∑math20

Differential geometry · Result 334

A smooth surface metric with no local isometric immersion in ℝ3

1 paperLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of A Smooth Metric with No Local Isometric Immersion into Three-Space

A Smooth Metric with No Local Isometric Immersion into Three-Space

OpenAI · 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.

Read PDF Download Source

Cite
@misc{OAI:A-Smooth-Metric-with-No-Local-Isometric-Immersion-into-Three-Space-September-24-2026,
  author = {{OpenAI}},
  title = {{A Smooth Metric with No Local Isometric Immersion into Three-Space}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-Smooth-Metric-with-No-Local-Isometric-Immersion-into-Three-Space-September-24-2026/paper.pdf}{OAI:A-Smooth-Metric-with-No-Local-Isometric-Immersion-into-Three-Space-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

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

Scope

The local isometric-immersion problem asks whether every smooth surface metric can be realized locally in Euclidean three-space. The formalized counterexample is a smooth positive-definite metric on \((-1,1)^2\) for which no neighborhood of the origin admits a smooth isometric immersion into \(\mathbb R^3\). The obstruction applies to every smooth candidate map on every such neighborhood.

Comparator links

ResultComparator statement
Smooth local isometric-immersion obstructionIsometricImmersion.lean

Scope note on GitHub →