Algebraic and complex geometry · Result 047

Zariski cancellation and affine fibrations over the complex numbers

1 paperLean

Constructs an integral complex affine fourfold \(X\not\cong\mathbb A^4\) with \(X\times\mathbb A^1\cong\mathbb A^5\), disproving affine-space cancellation over ℂ in dimension four. It also disproves the Dolgachev–Weisfeiler affine-fibration conjecture: smooth surjections \(X\to\mathbb A^1\) and \(\mathbb A^5\to\mathbb A^2\) have every residue-field fiber isomorphic to affine three-space but are not Zariski-locally trivial.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

An explicit failure of complex affine-space cancellation

OpenAI · September 23, 2026

We construct an explicit integral complex affine fourfold X with \(X\times\mathbb A^1\cong\mathbb A^5\) but \(X\not\cong\mathbb A^4\). This gives a negative answer to Zariski's affine-space cancellation problem over ℂ in dimension four. The same construction disproves the Stable Coordinate Conjecture in ambient dimension five and yields smooth 𝔸³-fibrations over 𝔸¹ and 𝔸² that are not Zariski-locally trivial. These fibrations disprove the Dolgachev–Weisfeiler affine-fibration conjecture over these bases.

Read PDF Download Source

Cite

@misc{OAI:An-explicit-failure-of-complex-affine-space-cancellation-September-23-2026,
  author = {{OpenAI}},
  title = {{An explicit failure of complex affine-space cancellation}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-explicit-failure-of-complex-affine-space-cancellation-September-23-2026/paper.pdf}{OAI:An-explicit-failure-of-complex-affine-space-cancellation-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

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

An explicit failure of complex affine-space cancellation

Scope

Affine-space cancellation asks whether \(X\times\mathbb A^1\cong\mathbb A^{n+1}\) forces \(X\cong\mathbb A^n\). The formalized result gives an explicit finite-type complex domain \(A\) of Krull dimension four with \(A[w]\cong\mathbb C[x_1,\ldots,x_5]\) but \(A\not\cong\mathbb C[x_1,\ldots,x_4]\). Thus adjoining one variable erases a genuine algebraic distinction.

The separate stable-coordinate and general line-bundle lifting consequences are not included.

Comparator links

Result	Comparator statement
Complex affine-space cancellation counterexample	ComplexCancellation.lean

Scope note on GitHub →