# A smooth surface metric with no local isometric immersion in ℝ<sup>3</sup>

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

- [A Smooth Metric with No Local Isometric Immersion into Three-Space](../../preprints/A-Smooth-Metric-with-No-Local-Isometric-Immersion-into-Three-Space-September-24-2026/paper.pdf)

## 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

| Result | Comparator statement |
| --- | --- |
| Smooth local isometric-immersion obstruction | [IsometricImmersion.lean](../ComparatorChallenges/IsometricImmersion.lean) |