View source for Local isometric immersion of smooth surfaces in three-space

'''Local isometric immersion of smooth surfaces in three-space''' is the question whether every smooth Riemannian surface can, near each point, be realized as a smooth surface in Euclidean three-space. A manuscript in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]), dated 24 September 2026, claims a negative answer: a smooth metric on a square for which no neighbourhood of the centre admits a smooth isometric immersion into '''R'''<sup>3</sup>. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper or a formal proof is not presented here as independent verification.

== Background ==
* As recounted in the introduction of the manuscript:
** The unrestricted smooth question appears in Yau's discussion of isometric embedding and as Problem 1.9 of Ghomi's survey. For analytic metrics the Janet–Cartan theorem gives local realizations. For smooth metrics, nonzero Gaussian curvature gives smooth local existence; Lin treated nonnegative curvature and a clean change of sign, Nakamura and Maeda proved smooth local existence under a clean change of sign, and more complicated zero sets have been treated under further restrictions.
** In low regularity, Nash–Kuiper flexibility gives ''C''<sup>1</sup> local realizations. Pogorelov constructed a ''C''<sup>2,1</sup> metric with no local ''C''<sup>2</sup> realization, and Nadirashvili and Yuan published a refinement with nonnegative curvature.
** An earlier preprint of Nadirashvili and Yuan states a smooth counterexample with nonpositive curvature and no ''C''<sup>3</sup> embedding, but their later published paper, and a subsequent discussion, leave the smooth question open; the manuscript records this discrepancy without resolving it and does not use the preprint.

== The original result ==
* '''Claim.''' Theorem A of ''A Smooth Metric with No Local Isometric Immersion into Three-Space'' states that there is a smooth positive-definite Riemannian metric ''g'' on (−1, 1)<sup>2</sup> such that no open neighbourhood of the origin admits a smooth isometric immersion into '''R'''<sup>3</sup>, and in particular no smooth isometric embedding. Theorem 5.3 states that the metric can be chosen to agree with the Euclidean metric to every order at the origin.
* '''Stated limits.''' The construction uses curvature of both signs and does not settle the problem under either restriction ''K'' ≥ 0 or ''K'' ≤ 0.
* ''Method, as described:'' any immersion gives scalar heights satisfying the Darboux equation. A uniform regularity estimate on caps, a thin oscillating perturbation of the metric and a Baire category argument give a metric for which no height in a suitable class exists on a whole square; the boundary-saddle argument of Nadirashvili and Yuan, applied to disks of negative curvature surrounded by such obstructed patches that accumulate at the origin, then excludes every local immersion.
* '''Source''' (openai/math repository, commit <code>7ef5c0c</code>): [https://github.com/openai/math/tree/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/preprints/A-Smooth-Metric-with-No-Local-Isometric-Immersion-into-Three-Space-September-24-2026 A Smooth Metric with No Local Isometric Immersion into Three-Space], dated 24 September 2026, 19 pages.
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/lean/docs/334.md lean/docs/334.md] states that the formalized counterexample is a smooth positive-definite metric on (−1, 1)<sup>2</sup> for which no neighbourhood of the origin admits a smooth isometric immersion into '''R'''<sup>3</sup>, and that the obstruction applies to every smooth candidate map on every such neighbourhood.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 29 October 2026)
|-
| 2026-10-07 || [https://lowrank.github.io/latent-seminar/OpenAI-Math/334-local-isometric-immersion-obstruction ''A smooth metric with no local immersion into three-space''], an article of the Latent Seminar blog at lowrank.github.io || Reading (exposition) || Explains intrinsic metrics and scalar heights, the necessary Darboux equation, the obstruction on a whole square, caps and two-sided regularity, the oscillating metric pulse, the Baire category step, boundary saddles and accumulation, and the Euclidean Taylor jet, with outlines of the key steps. || Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs.
|-
| 2026-10-12 || [https://kokunoyumeto.github.io/open-math-courses-public/courses/a-metric-with-no-local-isometric-immersion/ ''A metric with no local isometric immersion''], a course on Open Mathematics Courses ([https://github.com/kokunoyumeto/open-math-courses-public kokunoyumeto/open-math-courses-public]) || Reading (exposition) || Seven lessons with a complete proof of the manuscript's theorem: the height equation of an immersed surface; the construction of the metric from small squares that accumulate at the boundaries of disks of negative curvature; and the patch obstruction, through regularity across the curve where the curvature changes sign, energy estimates where the curvature is negative, and a rapidly oscillating perturbation of the metric excluded by Baire's theorem. || The lessons state that they were written by Claude Opus 5.5 (Anthropic) in October 2026 and self-checked by the writing AI; the course lists its status as author self-checked.
|-
| 2026-10-19 || ''AI Proved What?'', episode 334 [https://aiprovedwhat.com/episodes/334-no-local-r3/ Not even a piece fits in 3D?], remade version of 23 October 2026 || Reading (exposition) || Video explainer of the claim of a smooth metric on a square such that no neighbourhood of the centre, however small, has a smooth isometric immersion into three-space, with a metric that can match the flat plane to every order at the centre. The episode states that a counterexample with curvature of one sign, less smooth placements, failure away from the centre and an explicit formula are not claimed, the key perturbations coming from a category argument. || Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as a preprint: OpenAI, 19 pages, dated September 24, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: the main theorem, not the flat-to-every-order refinement. The page also states that the Lean formalization of the main theorem has about 450 files and 57,000 lines, not run by the site, that three outside projects re-ran the check, one with a second independent kernel, and that it found no public comment from specialists. It notes that the paper does not mention a second 2002 preprint by Nadirashvili, described in the joint preprint as giving a smooth metric of this kind, which the site could not find.
|}

== Notes ==
* The background summarizes the manuscript's own account of earlier work.
* 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]]