Lean formalization in OpenAI math repository (Result 049)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'A stable coordinate that is not a coordinate in four variables'. We construct an explicit degree-five polynomial over \mathbf C that is not a coordinate in four variables but becomes one after adjoining a single variable. This gives a counterexample to the stable coordinate conjecture in four variables. Every fiber is isomorphic to affine three-space, yet its embedding in affine four-space is not rectifiable. Thus the example also disproves the Abhyankar–Sathaye embedding conjecture in ambient dimension four.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 049). The Lean development was not rebuilt locally.