OpenAI claim summary for Math-423

Zariski Cancellation Problem (characteristic zero, dimension $\geq$ 3)

OpenAI's claim

An explicit complex affine fourfold is claimed to become affine five-space after one stabilization while itself failing to be affine four-space, with stable-coordinate and nontrivial affine-fibration consequences. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.

In $P=\mathbb C[p,s,u,F,J]$, define \[ x=s^2+u^3+p^2F,\qquad H=x^2F-(1+2sx)J-p^2J^2-pu,\qquad A=P/(H). \] OpenAI claims that $A$ is integral of dimension four and for an independent variable $w$, \[ A[w]\simeq\mathbb C^{[5]},\qquad A\not\simeq\mathbb C^{[4]}. \] The notation $\mathbb C^{[j]}$ denotes a polynomial algebra in $j$ variables. It also claims that $H$ is a coordinate of $P[w]$ but not of $P$, where coordinate means an element belonging to a polynomial coordinate system. These assertions give one-variable cancellation and stable-coordinate counterexamples in the indicated dimensions. Writing $X=\operatorname{Spec}A$, the affine-fibration corollary claims that \[ \pi:X\to\mathbb A^1,\quad x\mapsto p(x),\qquad \rho:\mathbb A^5\to\mathbb A^2,\quad z\mapsto(p(z),H(z)) \] are smooth and surjective with relative dimension three; every fiber over a base point $y$ is $\mathbb A^3_{\kappa(y)}$, yet neither map is locally a product with $\mathbb A^3$ in the Zariski topology. Thus the examples satisfy faithful flatness and geometric integrality of the fibers.

Outline of the argument

Manuscript 1 (family 047, 2026-09-23): A locally nilpotent derivation and an explicit inverse polynomial change give the cylinder isomorphism. To obstruct cancellation, a valuation along the exceptional parameter computes the associated graded affine modification; the resulting rigidity distinguishes the original coordinate ring from a polynomial algebra.

Formal verification

For family 047, the scope page documents the following selections. The selected construction is a four-dimensional complex domain whose one-variable polynomial extension is a five-variable polynomial ring, while the original ring is not polynomial. The other affine-fibration and stable-coordinate consequences are separate. The documented statement covers the main claim of manuscript 1. Its selected declaration also covers the clause used for this problem. Comparator files: ComplexCancellation.lean. Declarations: OAI.ComplexCancellation.main.

This site has not executed the Lean files or checked their dependencies. These descriptions report the scope of the linked declarations, rather than a new verification of the proofs.

Status caveat

OpenAI attributes these results to an internal model. Its release notice cautions that results lacking full formalization can contain mistakes. This site has not independently assessed the proofs; a solved label records the scope of the reported claim.

Sources

• OpenAI, An explicit failure of complex affine-space cancellation, 2026-09-23; citation key OAI:An-explicit-failure-of-complex-affine-space-cancellation-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main; Statement source: cor:stable-coordinate; Statement source: cor:affine-fibrations.
• Family 047: Lean scope.
• Comparator ComplexCancellation.json.
• Comparator ComplexCancellation.lean.
• OpenAI catalogue entry.