∑math20

Differential geometry · Result 333

Smooth isometric immersions of surfaces into ℝ4

1 paperLean

Every closed smooth Riemannian surface admits a smooth isometric immersion into ℝ4, resolving the closed-surface form of the four-dimensional isometric-immersion problem. This includes nonorientable surfaces and metrics of arbitrary Gaussian curvature.

Watch

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

Papers 1

First page of Smooth isometric immersions of closed surfaces into Euclidean four-space

Smooth isometric immersions of closed surfaces into Euclidean four-space

OpenAI · September 23, 2026

Every closed smooth Riemannian surface admits a smooth isometric immersion into Euclidean four-space, without an orientability assumption. This resolves the closed-surface form of the classical four-dimensional isometric-immersion problem.

Read PDF Download Source

Cite
@misc{OAI:Smooth-isometric-immersions-of-closed-surfaces-into-Euclidean-four-space-September-23-2026,
  author = {{OpenAI}},
  title = {{Smooth isometric immersions of closed surfaces into Euclidean four-space}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Smooth-isometric-immersions-of-closed-surfaces-into-Euclidean-four-space-September-23-2026/paper.pdf}{OAI:Smooth-isometric-immersions-of-closed-surfaces-into-Euclidean-four-space-September-23-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 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

ResultComparator statement
Smooth isometric immersion of every closed surface into four-spaceSurfaceImmersion.lean

Scope note on GitHub →