Browse › Differential geometry › 333 Smooth isometric immersions of surfaces into ℝ4
Smooth isometric immersions of closed surfaces into Euclidean four-space
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
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.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Follow-up works
- Kenta Kitamura (KitaKen1), Lean proof of smooth isometric embeddings into four-space (GitHub repository with manuscript "public draft 1", 9 October 2026). Claims to strengthen this paper's immersion result to a smooth isometric embedding of closed orientable surfaces in ℝ⁴, crediting the immersion result to OpenAI and providing a non-peer-reviewed Lean development with a self-reported Lean Comparator pass. [AI-generated per source]
Formalization
- OpenAI math release, Lean scope notes for family 333 (lean/docs/333.md). The scope note says the formalization proves that every closed smooth Riemannian surface admits a smooth isometric immersion into ℝ⁴, with no orientability assumption; the comparator statement is SurfaceImmersion.lean. [family-level]
- KitaKen1, Formalize smooth isometric embeddings of closed orientable surfaces in four-space and mark it as solved (google-deepmind/formal-conjectures PR #7211, opened 12 October 2026; open at time of collection). Adds the closed orientable embedding strengthening to formal-conjectures as "research solved", linking the external Lean proof above and resolving issue #7048; a reviewer asks for proof certification in the formal-conjectures environment before merge.
Possibly relevant literature (found by the agent, not checked)
- Qing Han and Marta Lewicka, Isometric immersions and applications (arXiv:2310.02566, October 2023; review for Notices of the AMS). Section 2.3 surveys the smallest target dimension (smooth embedding of compact surfaces in ℝ¹⁰ by Gromov and Günther, Poznyak's local version in ℝ⁴), giving context for the paper's comparison with Nash's dimension 17 and Gromov's ℝ⁵.
- Deane Yang, Gunther's proof of Nash's isometric embedding theorem (arXiv:math/9807169, July 1998). Exposition of Günther's proof, which avoids Nash–Moser iteration and improves the target dimension, relevant to the paper's dimension comparison and its remark that no global inverse of the linearized metric map is needed.
- Qing Han and Jia-Xing Hong, Isometric embedding of Riemannian manifolds in Euclidean spaces (AMS Mathematical Surveys and Monographs 130, 2006; library record). Standard monograph on local and global isometric embedding of surfaces, relevant to the paper's discussion of the Janet–Cartan local theory and its comparison with ℝ³.
Digests and expositions
- Latent Seminar, Smooth isometric immersions of surfaces into four-space (expository article, 2026-10-07). Explains the manuscript's primitive metric additions, smooth correction iteration and preservation of normal geometry, stating that it does not independently verify the proof or audit the Lean development. [family-level]
- Gradient Damage, Every OpenAI Math Result, Part 4 of 4: L = BPL, Integer Multiplication and 82 More (video, 2026-10-14). Chapter 75, from 25:44, gives a brief illustrated introduction to the four-dimensional immersion result, with animations identified as illustrations rather than proofs. [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 333
Independent sites; their content is not reviewed here.
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}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/333.md. The Lean statements have not been checked by people against the paper's claims.
Family 333: Smooth isometric immersions of surfaces into ℝ4
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.
This is the only paper in this family.