Motivation

An isometric immersion realizes an abstract Riemannian manifold as a surface in Euclidean space whose induced lengths are exactly the prescribed ones. How many dimensions are needed is a classical question. Nash showed that every compact Riemannian $n$-manifold embeds smoothly and isometrically in some Euclidean space; for surfaces his bound is $\mathbb R^{17}$ (Nash 1956). Gromov lowered the immersion dimension for closed surfaces to $\mathbb R^5$ (Partial Differential Relations, 1986, §3.2.4). Three dimensions do not suffice even locally in the smooth category, and Gromov recorded the question whether every smooth Riemannian surface admits a smooth isometric immersion into $\mathbb R^4$ (Gromov 2000, §I, Remark (d)), later attributing it to Chern around 1950 (Gromov 2015, p. 4).

This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 23, 2026 (source), which answers the compact, boundaryless form of that question: every closed smooth Riemannian surface admits a smooth isometric immersion into $\mathbb R^4$. The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Background

• 1926–1927 — Janet and Cartan: analytic Riemannian surfaces embed locally isometrically in $\mathbb R^3$ (Janet 1926; Cartan 1927).
• 1954–1955 — Nash and Kuiper: strictly short immersions in positive codimension can be uniformly approximated by $C^1$ isometric immersions (Nash 1954; Kuiper 1955).
• 1956 — Nash's smooth embedding theorem, dimension $n(3n+11)/2$, i.e. $17$ for surfaces.
• 1973 — Poznyak: $C^{3,\alpha}$ metrics on compact parts of simply connected planar domains admit $C^{2,\alpha}$ isometric immersions into $\mathbb R^4$ (Russ. Math. Surveys 1973).
• 1986 — Gromov: smooth isometric immersions of closed surfaces into $\mathbb R^5$.
• 2026 — Lewicka proves $C^{1,\alpha}$ flexibility in $\mathbb R^4$ for low-regularity metrics on disk-type planar domains (arXiv:2511.16305); a companion OpenAI preprint gives a smooth metric on a square with no local smooth isometric immersion into $\mathbb R^3$; the present preprint claims the closed-surface case in $\mathbb R^4$ (Theorem 1.1, p. 2).

Setting

A closed surface $M$ is a compact smooth two-dimensional manifold without boundary; it need not be orientable or connected. A Riemannian metric $g$ assigns to each $p\in M$ a positive definite inner product $g_p$ on $T_pM$, depending smoothly on $p$. A smooth map $F:M\to\mathbb R^4$ is an isometric immersion if

$$\langle dF_p(v),dF_p(w)\rangle=g_p(v,w)\qquad(p\in M,\ v,w\in T_pM).$$

Positive definiteness of $g$ forces $dF_p$ to be injective, so $F$ is an immersion; self-intersections are allowed.

Formalization targets

Goal: Theorem 1.1 (p. 2)

For every closed smooth Riemannian surface $(M,g)$ there is a $C^\infty$ map $F:M\to\mathbb R^4$ with $F^*\delta_4=g$, where $\delta_4=\sum_{i=1}^4dx_i^2$. In Lean this is OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_isometric_immersion.

Significance

The result itself. The theorem lowers Gromov's immersion dimension for closed surfaces from five to four, with no restriction on curvature or topology, and settles the closed case of the question Gromov attributes to Chern. Dimension four is the first codimension in which the smooth problem can have a global answer for all surfaces, since smooth metrics with no local isometric immersion into $\mathbb R^3$ exist. The open (noncompact) case of the question is not addressed.

Formalizing it. Mathlib now has smooth manifolds, tangent bundles and smooth Riemannian metrics, so the statement is expressible without custom geometry. A complete proof would add Whitney's immersion theorem, Sard's theorem in equal dimensions, metric decompositions into rank-one terms, Nash–Moser-type smoothing estimates, and oscillatory correction schemes; none of these are formalized at this level, and all are reusable in geometric analysis.

Difficulty

The isometric immersion equation $dF^{\mathsf T}dF=g$ is a nonlinear system of three equations in four unknown functions, and its linearization loses derivatives, so a direct implicit function argument fails. Convex integration in the Nash–Kuiper style produces only $C^1$ solutions. Poznyak's smooth theory works on planar domains with boundary, but on a closed surface the successive local corrections must remain compatible globally. The preprint keeps a nondegenerate normal geometry (a nonzero vector-valued second fundamental form) through every step, adds the metric deficit one positive rank-one term $a^2dx^2$ at a time via a velocity loop in a plane normal to $F_y$ and $F_{yy}$ (Proposition 3.1, p. 8; Proposition 7.1, p. 25), and then corrects the approximate metric exactly by a smoothing scheme that solves the linearized equation only on oscillatory modes (Proposition 5.1, p. 15). Nonorientable surfaces are handled by starting from an immersion into a small round $3$-sphere, whose radial direction is a global normal (Lemma 9.1, p. 35).

Formalization scope

• $M$ is a type with ChartedSpace (EuclideanSpace ℝ (Fin 2)) M and IsManifold 𝓘(ℝ, ℝ²) ∞ M, assumed compact, Hausdorff and second countable. Being modeled on $\mathbb R^2$ (not a half-space) encodes "without boundary"; no orientability or connectedness is assumed.
• The metric is Mathlib's Bundle.ContMDiffRiemannianMetric of class $C^\infty$ on the tangent bundle.
• The conclusion asks for ContMDiff … ∞ F and equality of the Euclidean inner product of mfderiv images with g.inner p v w for all tangent vectors; immersivity follows and is not stated separately.
• The statement is not trivialized: the conclusion is an exact pointwise identity for a smooth map, and the hypotheses are satisfied by every closed surface with any metric.

Selected references

• OpenAI, Smooth isometric immersions of closed surfaces into Euclidean four-space, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Smooth-isometric-immersions-of-closed-surfaces-into-Euclidean-four-space-September-23-2026/paper.pdf
• J. Nash, The imbedding problem for Riemannian manifolds, Ann. of Math. 63 (1956). https://doi.org/10.2307/1969989
• J. Nash, C¹-isometric imbeddings, Ann. of Math. 60 (1954). https://doi.org/10.2307/1969840
• M. Gromov, Partial Differential Relations, Springer (1986). https://doi.org/10.1007/978-3-662-02267-2
• M. Gromov, Spaces and questions, Geom. Funct. Anal. (2000). https://www.ihes.fr/~gromov/wp-content/uploads/2018/08/SpacesandQuestions.pdf
• M. Gromov, Geometric, algebraic and analytic descendants of Nash isometric embedding theorems (2015). https://www.ihes.fr/~gromov/wp-content/uploads/2018/08/nash-copy-Oct9.pdf
• E. G. Poznyak, Isometric immersions of two-dimensional Riemannian metrics in Euclidean space, Russian Math. Surveys (1973). https://doi.org/10.1070/RM1973v028n04ABEH001591
• M. Lewicka, Full flexibility of isometric immersions of metrics with low Hölder regularity in Poznyak theorem's dimension, arXiv:2511.16305v3 (2026). https://arxiv.org/abs/2511.16305v3
• H. Whitney, The singularities of a smooth n-manifold in (2n−1)-space, Ann. of Math. 45 (1944). https://doi.org/10.2307/1969266
• R. S. Hamilton, The inverse function theorem of Nash and Moser, Bull. AMS 7 (1982). https://doi.org/10.1090/S0273-0979-1982-15004-2