Algebraic and complex geometry · Result 049

A stable-coordinate counterexample in four variables

2 papersLean

Constructs a polynomial in four complex variables that is not a coordinate but becomes one after adjoining a single variable, disproving the Stable Coordinate conjecture in four variables. Every fiber is affine three-space, yet none of its embeddings is rectifiable, also disproving the Abhyankar–Sathaye conjecture even when all fibers are affine spaces.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

A stable coordinate that is not a coordinate in four variables

OpenAI · October 5, 2026

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.

Read PDF Download Source

Cite

@misc{OAI:A-stable-coordinate-that-is-not-a-coordinate-in-four-variables-October-5-2026,
  author = {{OpenAI}},
  title = {{A stable coordinate that is not a coordinate in four variables}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-stable-coordinate-that-is-not-a-coordinate-in-four-variables-October-5-2026/stable-coordinate-four-variables.pdf}{OAI:A-stable-coordinate-that-is-not-a-coordinate-in-four-variables-October-5-2026}},
  year = {2026}
}

An explicit noncoordinate polynomial with affine three-space zero fibre

OpenAI · September 24, 2026

We construct an explicit counterexample to the Abhyankar–Sathaye conjecture: a noncoordinate polynomial in four complex variables whose zero fibre is affine three-space. Adjoining variables gives counterexamples in every ambient dimension at least four.

Read PDF Download Source

Cite

@misc{OAI:An-explicit-noncoordinate-polynomial-with-affine-three-space-zero-fibre-September-24-2026,
  author = {{OpenAI}},
  title = {{An explicit noncoordinate polynomial with affine three-space zero fibre}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-explicit-noncoordinate-polynomial-with-affine-three-space-zero-fibre-September-24-2026/paper.pdf}{OAI:An-explicit-noncoordinate-polynomial-with-affine-three-space-zero-fibre-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The stable coordinate conjecture predicts that a polynomial that becomes a coordinate after adjoining variables was already a coordinate. The formalization gives an explicit degree-five polynomial in four complex variables that becomes a coordinate after adjoining one variable but is not a coordinate in four variables. Every fiber is isomorphic to affine three-space, yet no fiber can be carried to a coordinate hyperplane by an ambient polynomial automorphism.

The Abhyankar–Sathaye conjecture predicts that a polynomial defining an affine-space quotient must be an ambient coordinate. For every \(n\ge4\), the formalized counterexample gives \(F\in\mathbb C[x_1,\ldots,x_n]\) with quotient \(\mathbb C[x_1,\ldots,x_n]/(F)\cong\mathbb C[y_1,\ldots,y_{n-1}]\), although \(F\) is not a coordinate.

A companion gives \(n-1\) commuting, locally nilpotent derivations, linearly independent over the polynomial ring, whose common kernel is generated by the construction's explicit polynomial and contains no ambient coordinate. The extra \(n-4\) derivations are ordinary partial derivatives in the added variables. The three-variable case is not covered.

Comparator links

Result	Comparator statement
Noncoordinate polynomial in every dimension at least four	AbhyankarSathaye.lean
Commuting locally nilpotent derivations	CommutingDerivations.lean
Degree-five stable noncoordinate with nonrectifiable affine-space fibers	StableCoordinateFour.lean

Scope note on GitHub →