View source for Smooth isometric immersions of surfaces into four-space

'''Smooth isometric immersions of surfaces into four-space''' is the subject of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). The question is whether every closed smooth Riemannian surface can be realized smoothly and isometrically in Euclidean four-space; the manuscript attributes it to Gromov's writings, which trace the four-space surface question to Chern. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' Every closed smooth Riemannian surface admits a smooth isometric immersion into Euclidean four-space, with no orientability or curvature assumption. The manuscript states that this lowers the immersion dimension from five, in Gromov's construction, to four. Source: the manuscript [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Smooth-isometric-immersions-of-closed-surfaces-into-Euclidean-four-space-September-23-2026 Smooth isometric immersions of closed surfaces into Euclidean four-space], dated 23 September 2026.
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/333.md lean/docs/333.md] states that the formalization proves that every closed smooth Riemannian surface admits a smooth isometric immersion into four-space, with no orientability assumption, and that the statement asks for an immersion rather than an embedding.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math at commit <code>adc7f12</code>, tables at repository commit <code>cd0063d</code>, 13 October 2026) || Review (fidelity of the formal statements) || Rates this family "full": the Lean statement covers every compact Hausdorff second-countable smooth surface without boundary and every smooth Riemannian metric, with no orientability or curvature hypothesis. Its per-challenge table lists no Comparator run for the challenge <code>SurfaceImmersion</code>. || The review states that its ratings concern whether the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet.
|-
| 2026-10-09 (latest commit <code>65cbf4c</code>, 12 October 2026) || [https://github.com/KitaKen1/smooth-isometric-embeddings-r4 KitaKen1/smooth-isometric-embeddings-r4] (GitHub) || Extension (formal) || States a Lean proof that every closed orientable smooth surface with any smooth Riemannian metric admits a smooth isometric '''embedding''' into four-space, built on OpenAI's formalization of the immersion result together with formalized parts of a differential-geometry library and of the classification of surfaces. The README gives an AI-generated sketch in which the metric corrections preserve injectivity. || The repository describes the work as a proposed proof and records the author's run of the Lean Comparator.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]