# Smooth isometric immersions of surfaces into ℝ<sup>4</sup>

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

- [Smooth isometric immersions of closed surfaces into Euclidean four-space](../../preprints/Smooth-isometric-immersions-of-closed-surfaces-into-Euclidean-four-space-September-23-2026/paper.pdf)

## Scope

The formalization proves that every closed smooth Riemannian surface admits a smooth isometric immersion into $\mathbb R^4$. The differential preserves the Riemannian inner product on every tangent space. No orientability assumption is imposed, and the statement asks for an immersion rather than an embedding.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Smooth isometric immersion of every closed surface into four-space | [SurfaceImmersion.lean](../ComparatorChallenges/SurfaceImmersion.lean) |