Oct 6, 2026
Lean formalization in OpenAI math repository (Result 334)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'A Smooth Metric with No Local Isometric Immersion into Three-Space'. We construct a smooth positive-definite Riemannian metric on (-1,1)^2 that agrees with the Euclidean metric to every order at the origin, yet no neighborhood of the origin admits a smooth isometric immersion into Euclidean three-space. This gives a negative answer to the unrestricted smooth local isometric realization problem for surfaces.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 334). The Lean development was not rebuilt locally.