AI Proof WatchKeep up with AI contributions

A Smooth Metric with No Local Isometric Immersion into Three-Space

OpenAI

OpenAI’s Theorem A constructs a C∞ positive-definite metric g on (-1,1)^2 such that no open neighborhood of the origin admits a C∞ isometric immersion into R³. The paper also says g can agree with the Euclidean metric to every order at the origin. The Lean endpoint directly states the smooth positive metric and no-local-immersion claim; the flat-jet refinement is not part of that endpoint.

Sources for this record

What was already known

Ghomi asked whether every smooth surface metric locally embeds isometrically in R³. Known positive cases cover nonzero or cleanly changing curvature. A 2002 Nadirashvili–Yuan preprint claims a smooth counterexample, while later published accounts still describe the unrestricted question as open.

AI involvement AI-led

OpenAI is credited as author of the manuscript and formal proof. The release does not identify the individual model run or a human mathematical contributor. No named human proof checker or explainer is documented.

OpenAI is credited as manuscript author; the specific production history is not disclosed, so autonomy beyond this institutional attribution is unestablished.

Importance Notable

The formalized construction gives a smooth local obstruction in three-space.

Limitations

The 2002 preprint claims a stronger smooth example, leaving priority and distinct advance unresolved. The displayed Lean theorem covers nonimmersion, not the paper’s flat-to-all-orders refinement.

Technical verification Formal (Lean 4)

OpenAI’s Lean documentation identifies the exact smooth metric/no-local-immersion endpoint, and the public Main.lean contains a proof term for that statement. This is source-reported machine formalization, not a Lean run reproduced here; the flat-jet addendum is outside the displayed endpoint.

Formal checking

formal proof in OAI.Geometry.IsometricImmersion.Main, matching the comparator challenge statement

Checker
Lean 4 kernel as reported by OpenAI Math
Scope
exists_local_metric_without_local_immersion: a smooth positive metric on the coordinate square with no smooth local isometric immersion into R³ near zero
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Few

No named human explanation of the central cap and oscillatory obstruction is documented; the detailed manuscript and later tutorial are AI-authored or AI-credited, so human understanding is left at the evidence default.

Correction and publication history