# noncoordinate-polynomial

> OpenAI’s n ≥ 4 polynomial construction, with exact arithmetic, pinned Lean sources and the recorded comparator run.

Page: https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial

- Project: [sciencehub-team/noncoordinate-polynomial](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial.md)
- Authors: ScienceHub
- Subjects: geometry-and-topology
- Topics: algebraic-geometry, formal-mathematics, lean, abhyankar-sathaye
- 0 stars, 0 forks
- Built on by 0 public projects: https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/sources.md
- Source: https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/source
- Updated 29 Oct 2026

## Notebook

Text the notebook's authors wrote, its cells as Python, and the outputs it produced when it last ran in a browser and was saved.

The script header: the dependencies the notebook declares (PEP 723) and the app it defines.

```python
# /// script
# requires-python = ">=3.11"
# dependencies = ["marimo>=0.25.1"]
# ///

import marimo

__generated_with = "0.25.1"
app = marimo.App(width="medium", app_title="A polynomial that cuts out affine space but is not a coordinate")
```

```python
import hashlib
import json
import re
from fractions import Fraction
from pathlib import Path

LEAN = Path("lean")
EVIDENCE = Path("evidence/openai-049.json")
EVIDENCE_MISSING = (
    "This project has no record of a run from main yet. The record will be "
    "`evidence/openai-049.json` in this project, and this cell will show it."
)
OPENAI_COMMIT = "7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a"

# Each file with the SHA-256 that the build pinned before compiling it.
LEAN_FILES = {
    "ComparatorChallenges/AbhyankarSathaye.lean": "a7db47dbd441d730d082f3cae61a2d7f22fd37aae46429dc269b290f262504c6",
    "ComparatorChallenges/AbhyankarSathaye.json": "c7e954153e064582ebcbaf85deacc29f933dca1c7188e90a6a78eb17b929148f",
    "OAI/AlgebraicGeometry/AbhyankarSathaye/Identities.lean": "821185a3f4e290139437d03fac7e77bd07c0c17ebde1bb12557e3a4b17791bb0",
    "OAI/AlgebraicGeometry/AbhyankarSathaye/CriticalPoint.lean": "8482fed2b765a9cdcbb651302ce0f1dd9916a009bd785bca371640b01974e33b",
    "OAI/AlgebraicGeometry/AbhyankarSathaye/NonCoordinate.lean": "4d65effda7f183af78ad4c46ad3ea01cf9eb9ec8cc9aba113160a2e61f3c2ac8",
    "OAI/AlgebraicGeometry/AbhyankarSathaye/LiftingIdentities.lean": "96493e2252652628a81442007f1166ac4c9556e7a64ba85b7bca80d1abff0ccb",
    "OAI/AlgebraicGeometry/AbhyankarSathaye/Quotient.lean": "a9ca84c304ea3e6c692f101399eb0be4510e9942d9df4c81d1a0fb36efafe065",
    "OAI/AlgebraicGeometry/AbhyankarSathaye/Reconstruction.lean": "e3d5adf0a453e79048927bdef4de1f2984eb8ebe8879414614c45210f441429d",
    "OAI/AlgebraicGeometry/AbhyankarSathaye/LinearElimination.lean": "213837b77e099684e5796964f349a987e5074de3c7958a685cb1e279041f9d7a",
    "OAI/AlgebraicGeometry/AbhyankarSathaye/Lifting.lean": "1572068ef8754f570b77049940b69f9c6fe4450390f818394c40f5a9af1dd323",
    "OAI/AlgebraicGeometry/AbhyankarSathaye/Plane.lean": "048bdff674496e8f346f41c505a1f3ff74f2e29d3a50f12e005efe2ab6f82ed3",
    "OAI/AlgebraicGeometry/AbhyankarSathaye/Presentation.lean": "0e7b8ed7ab6d7634969b226198f273458b4a7c0b5737a803584f5c17a8e1b6a0",
    "OAI/AlgebraicGeometry/AbhyankarSathaye/Fiber.lean": "d00e86d6250e5f0b63af7a486134d58fe2d60b50c1ff8c6f1d109f6d44156c49",
    "OAI/AlgebraicGeometry/AbhyankarSathaye/FiberFormulas.lean": "172b6d1609d4a0c7b3ccd56011ca4a5135e789e25801b6b77038f7ff83699876",
    "OAI/AlgebraicGeometry/AbhyankarSathaye/Stabilization.lean": "c679b604d36b8d6275e0b3924dd2269d25e08f4cda4b29d3770997f1dc7ada99",
    "OAI/AlgebraicGeometry/AbhyankarSathaye/LinearPresentation.lean": "0bd3cd657eb53f988e3343a1671038c88117fa220a7cd9f85322c34fc35db8e8",
    "OAI/AlgebraicGeometry/AbhyankarSathaye/Counterexample.lean": "75c94499e489e26905564aa853cde0875bbab6354d29aff7ebb8bf80899bb04f",
}
```

```python
class Dual:
    """A number a + b·ε with ε² = 0. Evaluating a polynomial at x + ε gives its derivative at x in b, exactly."""

    def __init__(self, a, b=0):
        self.a, self.b = Fraction(a), Fraction(b)

    @staticmethod
    def _lift(other):
        return other if isinstance(other, Dual) else Dual(other)

    def __add__(self, other):
        other = Dual._lift(other)
        return Dual(self.a + other.a, self.b + other.b)

    __radd__ = __add__

    def __neg__(self):
        return Dual(-self.a, -self.b)

    def __sub__(self, other):
        return self + (-Dual._lift(other))

    def __rsub__(self, other):
        return Dual._lift(other) - self

    def __mul__(self, other):
        other = Dual._lift(other)
        return Dual(self.a * other.a, self.a * other.b + self.b * other.a)

    __rmul__ = __mul__

    def __pow__(self, n: int):
        result = Dual(1)
        for _ in range(n):
            result = result * self
        return result
```

```python
def S(h, u, v, w):
    """The quotient (x² + y³)/h, as `S` in Identities.lean."""
    return 2 * u**3 * v + 3 * u**4 * w + h * (v**2 - 3 * u**2 * w**2) + h**2 * w**3
```

```python
def P(x, y, s):
    """The correction term p, as `P` in Identities.lean. Not the critical point P of the text."""
    return -2 * s**2 * x + 3 * s * y**2 - 3 * s**3 * y
```

```python
def construction(h, u, v, w) -> dict:
    """x, y, s, p and F at one point, in the order of Identities.lean."""
    x = u**3 + h * v
    y = -(u**2) + h * w
    s = S(h, u, v, w)
    p = P(x, y, s)
    return {"x": x, "y": y, "s": s, "p": p, "F": h - p - 1}
```

```python
def gradient(point) -> list:
    """The four partial derivatives of F at a point, exact over the rationals."""
    partials = []
    for i in range(4):
        seeded = [Dual(c, 1 if j == i else 0) for j, c in enumerate(point)]
        partials.append(construction(*seeded)["F"].b)
    return partials
```

```python
def load_evidence(path: Path = EVIDENCE) -> str:
    """The record of a Lean proof check run as Markdown, or a sentence saying why there is none to show."""
    try:
        evidence = json.loads(path.read_text(encoding="utf-8"))
    except FileNotFoundError:
        return EVIDENCE_MISSING
    except (OSError, ValueError) as error:
        return f"`{path}` cannot be read: {error}."
    try:
        return evidence_summary(evidence)
    except (AttributeError, KeyError, TypeError, ValueError, StopIteration):
        return f"`{path}` is not a record of the kind this notebook reads."
```

```python
def scrub(text: str) -> str:
    """Text from a run record with the owner of ScienceHub's CI repository and image replaced by OWNER."""
    keep = {"ghcr.io", "github.com", "api.github.com", "docker.io", "v2", "repos"}

    def owner(match):
        return match.group(0) if match.group(1) in keep else "OWNER/"

    return re.sub(r"([\w.-]+)/(?=sciencehub(?:-lean)?\b)", owner, text)
```

```python
def plural(count: int, word: str) -> str:
    return f"{count} {word}" + ("" if count == 1 else "s")
```

```python
def finished(stamp: str) -> str:
    """An ISO time as a date like 28 Oct 2026."""
    from datetime import datetime

    moment = datetime.fromisoformat(str(stamp).replace("Z", "+00:00"))
    return f"{moment.day} {moment.strftime('%b %Y')}"
```

```python
def image_digest(image) -> str:
    """The image's digest alone, from a record that gives a digest or, in its first format, a full reference."""
    if isinstance(image, dict):
        image = image.get("digest") or image["ref"]
    digest = str(image).rsplit("@", 1)[-1]
    if not digest.startswith("sha256:"):
        raise ValueError(digest)
    return digest
```

```python
def evidence_summary(evidence: dict) -> str:
    """The record as Markdown. It names the run by number and the image by digest only.

    A run that was not accepted is shown by its outcome and the reason each runtime gives;
    the table is for accepted runs, whose records have every field it reads.
    """
    if not str(evidence["schema"]).startswith("sciencehub.lean-proof-evidence/"):
        raise ValueError(evidence["schema"])
    run = evidence["run"]
    ref = run.get("ref")
    if ref == "refs/heads/main":
        where = "**The run from main.**"
    else:
        where = f"**A run not from main.** This record is from `{scrub(str(ref))}`." if ref else "**A run not from main.** This record names no ref."
    head = (
        f"{where} Run {int(run.get('run_id', run.get('id')))}"
        + (f", finished {finished(run['finished_at'])}" if run.get("finished_at") else "")
        + ", in ScienceHub's CI "
        f"repository, which is private. Outcome: **{evidence['outcome']}**."
    )
    if evidence["outcome"] != "accepted":
        lines = [head]
        unmatched = [f["path"] for f in evidence["source"]["files"] if not f["match"]]
        if unmatched:
            lines += ["", f"{len(unmatched)} file{'s' if len(unmatched) != 1 else ''} did not match its pinned SHA-256: " + ", ".join(f"`{u}`" for u in unmatched) + "."]
        for name, result in evidence["runtimes"].items():
            if result["outcome"] != "accepted":
                if result.get("stage") == "not run":
                    lines += ["", f"Under {name} the proof was not run."]
                    continue
                lines += ["", f"Under {name} the run stopped at {result.get('stage')}."]
                if result.get("reason") is not None:
                    reason = scrub(str(result["reason"]))[:1500]
                    fence = "`" * max(3, 1 + max((len(m) for m in re.findall(r"`+", reason)), default=0))
                    lines += ["", f"{fence}text", reason, fence]
        return "\n".join(lines)
    runtime = evidence["runtimes"]["runsc"]
    versions = runtime["lean"]["versions_json"]
    modules = runtime["modules"]
    files = evidence["source"]["files"]
    axioms = "; ".join(
        f"`{name}`: " + ", ".join(f"`{a}`" for a in entry["axioms"])
        for name, entry in runtime["axioms"]["theorems"].items()
    )
    default, paranoid = runtime["comparator"]["default"], runtime["comparator"]["paranoid"]
    others = ", ".join(f"{name} {r['outcome']}" for name, r in evidence["runtimes"].items() if name != "runsc")
    rows = [
        ("Image", f"`{image_digest(evidence['image'])}`"),
        ("Lean", f"{versions['lean']} (commit `{versions['lean_commit'][:7]}`)"),
        ("Mathlib", f"{versions['mathlib']} (commit `{versions['packages']['mathlib'][:7]}`)"),
        ("Files fetched", f"{sum(1 for f in files if f['match'])} of {len(files)} matched their pinned SHA-256"),
        ("Modules built", f"{sum(1 for m in modules if m['exit'] == 0)} of {len(runtime['build_order'])}, " + plural(sum(int(m["warnings"]) for m in modules), "warning")),
        ("Axioms", axioms),
        ("Comparator, default mode", f"{default['verdict']} in {default['comparator_seconds']} s"),
        ("Comparator, paranoid mode", f"{paranoid['verdict']} in {paranoid['comparator_seconds']} s: " + ", ".join(f"{k} {v}" for k, v in paranoid["kernels"].items())),
        ("The challenge as its own solution", f"{runtime['control']['verdict']} ({scrub(str(runtime['control']['reason']))})"),
        ("Challenge export", f"`{runtime['challenge']['export_sha256']}`"),
        ("Solution export", f"`{runtime['solution']['export_sha256']}`"),
    ]
    return "\n".join(
        [
            head,
            "",
            "The table shows the run in a gVisor sandbox (runsc)" + (f"; the same proof under {others}." if others else "."),
            "",
            "| | Value |",
            "| --- | --- |",
            *(f"| {label} | {value.replace('|', chr(92) + '|')} |" for label, value in rows),
            "",
            "The comparator's own sandbox is off in these runs, as in the earlier run below; separate "
            "containers, with the judge seeing only the two exports, take its place. The two export hashes "
            "are what you can compare without our runners; the steps follow.",
        ]
    )
```

```python
import marimo as mo
```

### A polynomial that cuts out affine space but is not a coordinate

Take a polynomial $F$ in $n$ complex variables whose zero set is a copy of
affine $(n-1)$-space, in the strong algebraic sense that
$\mathbb C[x_1,\dots,x_n]/(F)$ is a polynomial ring in $n-1$ variables.
Is there always a polynomial change of coordinates of $\mathbb C^n$ that
turns $F$ into $x_1$? The Abhyankar–Sathaye conjecture says yes.

A preprint by OpenAI dated 24 Sep 2026 claims a counterexample in four
variables, and with it one in every dimension $n \ge 4$. OpenAI's
repository `openai/math` publishes a Lean statement of this claim and a
proof of that statement. A second preprint, dated 5 Oct 2026, gives,
according to OpenAI's summary in its `CONTENTS.md`, a different
four-variable counterexample of degree five: a stable coordinate that
is not a coordinate.

This notebook shows the Lean statement, explains the construction
behind it, lets you evaluate the polynomial at its critical point, and
reproduces the Lean source in full. It also says what running Lean on
these files does and does not tell you.

#### The question

**Coordinates.** Write $R_n = \mathbb C[x_1,\dots,x_n]$. A polynomial
$f \in R_n$ is a *coordinate* if there are $f_2,\dots,f_n$ with
$\mathbb C[f, f_2, \dots, f_n] = R_n$. Equivalently, some automorphism
of $R_n$ as a $\mathbb C$-algebra sends a variable $x_i$ to $f$; or,
geometrically, some polynomial automorphism of $\mathbb C^n$, with a
polynomial inverse, has $f$ as its first component. The polynomial
$x_1 + x_2^7$ is a coordinate; so is $x_1 + g(x_2,\dots,x_n)$ for any $g$.

If $f$ is a coordinate, the automorphism carries the hypersurface
$f = 0$ onto the hyperplane $x_1 = 0$, so
$R_n/(f) \cong \mathbb C[y_1,\dots,y_{n-1}]$. The same holds for every
fibre $f = c$.

**The conjecture.** The Abhyankar–Sathaye conjecture asks for the
converse: if $R_n/(f) \cong \mathbb C[y_1,\dots,y_{n-1}]$ as
$\mathbb C$-algebras, is $f$ a coordinate? Geometrically: can every
closed embedding of $\mathbb C^{n-1}$ as a hypersurface in
$\mathbb C^n$ be straightened by an automorphism of $\mathbb C^n$? For
$n = 2$ the answer is yes; this is the theorem of Abhyankar and Moh and
of Suzuki on embeddings of the line in the plane.

**What is claimed.** The preprint claims, and OpenAI's Lean statement
below is written to state, that for every $n \ge 4$ there is an
$F \in R_n$ with $R_n/(F) \cong \mathbb C[y_1,\dots,y_{n-1}]$ that is
not a coordinate. The example is explicit: a polynomial in four
variables, and the same polynomial in more variables for larger $n$.

**What is not covered.** The case $n = 3$. The first preprint says
"The three-variable case is not addressed."

#### The formal statement

For this result OpenAI publishes a *challenge file*: the statement
alone, with `sorry` in place of the proof. It imports only Mathlib.
This is `ComparatorChallenges/AbhyankarSathaye.lean` as published:

```lean
import Mathlib.Algebra.MvPolynomial.CommRing
import Mathlib.Basic.Complex.Basic
import Mathlib.RingTheory.Ideal.Quotient.Operations

namespace OAI

namespace AbhyankarSathaye

/-- In every dimension at least four, a polynomial can define affine space
without being a coordinate of the ambient polynomial ring. -/
theorem exists_noncoordinate_polynomial (n : ℕ) (hn : 4 ≤ n) :
    ∃ F : MvPolynomial (Fin n) ℂ,
      Nonempty ((MvPolynomial (Fin n) ℂ ⧸ Ideal.span {F}) ≃ₐ[ℂ]
        MvPolynomial (Fin (n - 1)) ℂ) ∧
      ¬ ∃ (equiv : MvPolynomial (Fin n) ℂ ≃ₐ[ℂ] MvPolynomial (Fin n) ℂ)
        (index : Fin n), equiv (MvPolynomial.X index) = F := by
  sorry

end AbhyankarSathaye

end OAI
```

Read it a line at a time.

- `(n : ℕ) (hn : 4 ≤ n)`: for every natural number $n$ with $n \ge 4$.
- `MvPolynomial (Fin n) ℂ` is $R_n$: polynomials with complex
  coefficients in variables `X 0`, …, `X (n-1)`.
- `∃ F : MvPolynomial (Fin n) ℂ, … ∧ …`: there is a polynomial $F$
  with the two properties that follow. The statement only asserts that
  such an $F$ exists; the proof supplies one.
- `MvPolynomial (Fin n) ℂ ⧸ Ideal.span {F}` is the quotient ring
  $R_n/(F)$.
- `A ≃ₐ[ℂ] B` is the type of isomorphisms of $\mathbb C$-algebras from
  $A$ to $B$, and `Nonempty (…)` says there is at least one. So the first
  property is $R_n/(F) \cong \mathbb C[y_1,\dots,y_{n-1}]$. The `n - 1`
  is subtraction of natural numbers, which is the usual one because
  $n \ge 4$.
- `¬ ∃ (equiv : …) (index : Fin n), equiv (MvPolynomial.X index) = F`:
  there is no $\mathbb C$-algebra automorphism of $R_n$ that sends some
  variable to $F$. That is, $F$ is not a coordinate, in the sense
  defined above.

The statement uses Mathlib's definitions only. Whether it says what the
conjecture says is a question about these few lines, not about the 1,445
lines of Lean below them.

#### The construction

Work in $R = \mathbb C[h,u,v,w]$, in the variable order the Lean files use.
Start from the cusp $(u^3, -u^2)$, on which $X^2 + Y^3 = 0$, and perturb
both entries by multiples of $h$:

$$x = u^3 + hv, \qquad y = -u^2 + hw.$$

Then $x^2 + y^3$ vanishes modulo $h$, and the quotient is the polynomial

$$s = 2u^3v + 3u^4w + h\,(v^2 - 3u^2w^2) + h^2w^3, \qquad x^2 + y^3 = hs.$$

With $p = -2s^2x + 3sy^2 - 3s^3y$, the counterexample is

$$F = h - p - 1.$$

Expanded, $F$ has degree 17 in $h, u, v, w$ (our computation, not a claim
of the sources). Lean proves the identity above and
$(x + s^3)^2 + (y - s^2)^3 = x^2 + y^3 - sp$ with `ring`
(`cusp_universal` and `shift_universal` in `Identities.lean`), and from
them, in `ambient`,

$$(x + s^3)^2 + (y - s^2)^3 = s\,(1 + F).$$

**The zero fibre is affine 3-space.** On $F = 0$ we have $h = 1 + p$.
The proof builds the isomorphism $R/(F) \cong \mathbb C[X,Y,T]$ in
stages. `Presentation.lean` rewrites $R/(F)$ with the auxiliary letters
$x$, $y$, $s$ alongside $u$, $v$, $w$. The algebra cut out by
$h = 1 + p(x,y,s)$ and $x^2 + y^3 = hs$ in the four letters $h$, $x$,
$y$, $s$ is a polynomial ring in $x + s^3$ and $y - s^2$ (`Plane.lean`).
Over that ring, the equations $u^3 + hv = x$, $-u^2 + hw = y$ and
$S(h,u,v,w) = s$ define a polynomial ring in one more variable
(`Lifting.lean`), because $x^2 + y^3 = hs$ and $\alpha h + \beta y = 1$
hold in that ring for explicit polynomials $\alpha$ and $\beta$
(`bezout_certificate` in `Identities.lean`, applied as `bezout` in
`Plane.lean`). `FiberFormulas.lean` records the result: the inverse
isomorphism sends $X$, $Y$, $T$ to $x + s^3$, $y - s^2$ and
$\alpha u + \beta (v + uw)$.

**$F$ is not a coordinate.** At the point
$P = (h,u,v,w) = (2, 0, -\tfrac12, \tfrac12)$,

$$x = -1, \quad y = 1, \quad s = 1, \quad p = 2, \quad F = -1,$$

so $x + s^3 = 0$ and $y - s^2 = 0$. Differentiate the ambient identity
in any variable:

$$2(x+s^3)\,d(x+s^3) + 3(y-s^2)^2\,d(y-s^2) = (1+F)\,ds + s\,dF.$$

At $P$ the left side is zero, $1 + F = 0$ and $s = 1$, so $dF(P) = 0$:
every partial derivative of $F$ vanishes at $P$
(`critical_derivatives` in `CriticalPoint.lean`).

A coordinate has no such point. If an automorphism $\varphi$ of
$\mathbb C^n$ has $F$ as its first component, the chain rule applied to
$\varphi^{-1} \circ \varphi = \mathrm{id}$ shows that the Jacobian
matrix of $\varphi$ is invertible at every point, so its first row,
$\nabla F$, is never zero. `NonCoordinate.lean` proves the algebraic form
of this for any nontrivial commutative ring of coefficients
(`polynomial_chain_rule`, `no_coordinate_of_critical`).

The critical point lies on the fibre $F = -1$, not on $F = 0$. The zero
fibre is smooth, as affine space is; the obstruction is in how $F$
behaves on the rest of $\mathbb C^4$.

**More variables.** For every $n \ge 4$, `Stabilization.lean` takes
the same $F$ in $\mathbb C[h,u,v,w,z_1,\dots,z_{n-4}]$, renaming its
variables into the first four of $n$ (for $n = 4$ this is $F$ itself).
The quotient gains the $z_i$ as free variables, and $(P, 0, \dots, 0)$
is still a critical point, since $F$ does not depend on the $z_i$.

#### Evaluate $F$ yourself

Move the point. The cell below computes $x$, $y$, $s$, $p$, $F$ and the
four partial derivatives of $F$ in exact rational arithmetic, with
Python's `fractions` and dual numbers for the derivatives, so no
rounding is involved. It starts at the critical point $P$. Try
$(1, 0, 0, 0)$, which lies on the zero fibre, to see a point where the
gradient is not zero.

This is our own spot check of facts the proof uses. It is not part of
the proof and does not replace it.

```python
h_in = mo.ui.slider(-3, 3, step=0.25, value=2, label="h", show_value=True)
u_in = mo.ui.slider(-2, 2, step=0.25, value=0, label="u", show_value=True)
v_in = mo.ui.slider(-2, 2, step=0.25, value=-0.5, label="v", show_value=True)
w_in = mo.ui.slider(-2, 2, step=0.25, value=0.5, label="w", show_value=True)
mo.vstack([h_in, u_in, v_in, w_in])
```

```python
point = [Fraction(_c.value) for _c in (h_in, u_in, v_in, w_in)]
values = construction(*point)
grad = gradient(point)
_left = (values["x"] + values["s"] ** 3) ** 2 + (values["y"] - values["s"] ** 2) ** 3
_right = values["s"] * (1 + values["F"])

_lines = [
    f"At $(h,u,v,w) = ({', '.join(str(_c) for _c in point)})$:",
    "",
    "| Quantity | Exact value |",
    "| --- | --- |",
    *(f"| ${_name}$ | {values[_name]} |" for _name in ("x", "y", "s", "p", "F")),
    *(f"| $\\partial F/\\partial {_var}$ | {_g} |" for _var, _g in zip("huvw", grad)),
    "",
    "Every partial derivative is zero: this is a critical point of $F$."
    if all(_g == 0 for _g in grad)
    else "The gradient is not zero here.",
    "",
    f"The ambient identity at this point: $(x+s^3)^2 + (y-s^2)^3 = {_left}$ and $s(1+F) = {_right}$.",
]
mo.md("\n".join(_lines))
```

Output:

```text
<span class="markdown prose dark:prose-invert contents"><span class="paragraph">At <marimo-tex class="arithmatex">||((h,u,v,w) = (2, 0, -1/2, 1/2)||)</marimo-tex>:</span>
<table>
<thead>
<tr>
<th>Quantity</th>
<th>Exact value</th>
</tr>
</thead>
<tbody>
<tr>
<td><marimo-tex class="arithmatex">||(x||)</marimo-tex></td>
<td>-1</td>
</tr>
<tr>
<td><marimo-tex class="arithmatex">||(y||)</marimo-tex></td>
<td>1</td>
</tr>
<tr>
<td><marimo-tex class="arithmatex">||(s||)</marimo-tex></td>
<td>1</td>
</tr>
<tr>
<td><marimo-tex class="arithmatex">||(p||)</marimo-tex></td>
<td>2</td>
</tr>
<tr>
<td><marimo-tex class="arithmatex">||(F||)</marimo-tex></td>
<td>-1</td>
</tr>
<tr>
<td><marimo-tex class="arithmatex">||(\partial F/\partial h||)</marimo-tex></td>
<td>0</td>
</tr>
<tr>
<td><marimo-tex class="arithmatex">||(\partial F/\partial u||)</marimo-tex></td>
<td>0</td>
</tr>
<tr>
<td><marimo-tex class="arithmatex">||(\partial F/\partial v||)</marimo-tex></td>
<td>0</td>
</tr>
<tr>
<td><marimo-tex class="arithmatex">||(\partial F/\partial w||)</marimo-tex></td>
<td>0</td>
</tr>
</tbody>
</table>
<span class="paragraph">Every partial derivative is zero: this is a critical point of <marimo-tex class="arithmatex">||(F||)</marimo-tex>.</span>
<span class="paragraph">The ambient identity at this point: <marimo-tex class="arithmatex">||((x+s^3)^2 + (y-s^2)^3 = 0||)</marimo-tex> and <marimo-tex class="arithmatex">||(s(1+F) = 0||)</marimo-tex>.</span></span>
```

```python
mo.md(rf"""
## The Lean source

Below are all 15 files of the proof and the challenge with its
comparator configuration, shown as published in
[openai/math](https://github.com/openai/math/tree/{OPENAI_COMMIT}/lean)
at commit `{OPENAI_COMMIT[:7]}`. They are OpenAI's work, licensed under
the Apache License 2.0. This project keeps them unchanged in its `lean/`
folder, with the licence text in `lean/LICENSE` and a statement of
changes (none) in `lean/NOTICE`. The challenge and its configuration
come first, then the proof files in the order they build;
`Counterexample.lean` holds the main theorem.

Each heading shows the file's SHA-256 as computed here and whether it
matches the hash the earlier run pinned before compiling.
""")
```

Output:

```text
<span class="markdown prose dark:prose-invert contents"><h2 id="the-lean-source">The Lean source</h2>
<span class="paragraph">Below are all 15 files of the proof and the challenge with its
comparator configuration, shown as published in
<a href="https://github.com/openai/math/tree/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/lean" rel="noopener noreferrer" target="_blank">openai/math</a>
at commit <code>7ef5c0c</code>. They are OpenAI's work, licensed under
the Apache License 2.0. This project keeps them unchanged in its <code>lean/</code>
folder, with the licence text in <code>lean/LICENSE</code> and a statement of
changes (none) in <code>lean/NOTICE</code>. The challenge and its configuration
come first, then the proof files in the order they build;
<code>Counterexample.lean</code> holds the main theorem.</span>
<span class="paragraph">Each heading shows the file's SHA-256 as computed here and whether it
matches the hash the earlier run pinned before compiling.</span></span>
```

````python
_panels = {}
for _path, _pinned in LEAN_FILES.items():
    _file = LEAN / _path
    if not _file.exists():
        _panels[_path] = mo.md(
            f"`lean/{_path}` is missing. It ships with this project; download the project to read it."
        )
        continue
    _bytes = _file.read_bytes()
    _digest = hashlib.sha256(_bytes).hexdigest()
    _match = "matches the pinned hash" if _digest == _pinned else "does not match the pinned hash"
    _lines = _bytes.decode("utf-8").count("\n")
    _language = "json" if _path.endswith(".json") else "lean"
    _title = f"{_path} · {_lines} lines · sha256 {_digest[:12]}… {_match}"
    _panels[_title] = mo.md(f"```{_language}\n{_bytes.decode('utf-8')}```")
mo.accordion(_panels)
````

Output:

```text
lean/ComparatorChallenges/AbhyankarSathaye.lean is missing. It ships with this project; download the project to read it.
lean/ComparatorChallenges/AbhyankarSathaye.json is missing. It ships with this project; download the project to read it.
lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Identities.lean is missing. It ships with this project; download the project to read it.
lean/OAI/AlgebraicGeometry/AbhyankarSathaye/CriticalPoint.lean is missing. It ships with this project; download the project to read it.
lean/OAI/AlgebraicGeometry/AbhyankarSathaye/NonCoordinate.lean is missing. It ships with this project; download the project to read it.
lean/OAI/AlgebraicGeometry/AbhyankarSathaye/LiftingIdentities.lean is missing. It ships with this project; download the project to read it.
lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Quotient.lean is missing. It ships with this project; download the project to read it.
lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Reconstruction.lean is missing. It ships with this project; download the project to read it.
lean/OAI/AlgebraicGeometry/AbhyankarSathaye/LinearElimination.lean is missing. It ships with this project; download the project to read it.
lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Lifting.lean is missing. It ships with this project; download the project to read it.
lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Plane.lean is missing. It ships with this project; download the project to read it.
lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Presentation.lean is missing. It ships with this project; download the project to read it.
lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Fiber.lean is missing. It ships with this project; download the project to read it.
lean/OAI/AlgebraicGeometry/AbhyankarSathaye/FiberFormulas.lean is missing. It ships with this project; download the project to read it.
lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Stabilization.lean is missing. It ships with this project; download the project to read it.
lean/OAI/AlgebraicGeometry/AbhyankarSathaye/LinearPresentation.lean is missing. It ships with this project; download the project to read it.
lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Counterexample.lean is missing. It ships with this project; download the project to read it.
```

#### How we ran it

This section reports the runs the ScienceHub team makes in CI. It is
not a status the site attaches to this notebook.

OpenAI's files pin Lean v4.34.1 and Mathlib at commit `d13f23b`.
ScienceHub's Lean image carries Lean v4.35.0 and Mathlib v4.35.0. In the
earlier run below, the 15 files built there without any change to their
source.

Each run uses Lean's comparator (`lake comparator`, shipped with Lean
v4.35.0) on two inputs: the challenge file above, and a solution file
that imports `Counterexample.lean`. The comparator

1. compares the theorem's statement in the solution with the
   challenge's, together with every definition that statement mentions,
   and accepts only an exact match, so the proof cannot have changed what
   is being proved;
2. walks everything the proof uses and rejects any axiom outside
   `propext`, `Quot.sound` and `Classical.choice`, the list OpenAI's
   `AbhyankarSathaye.json` also gives. A `sorry` is an axiom too, so it
   would be rejected;
3. replays the whole proof in Lean's kernel and, in paranoid mode, in
   five more: Lean's kernel in its paranoid setting, lean4lean,
   nanoda, con-leche and con-ron. All six must accept. Apart from
   Lean's own kernel and its paranoid setting, the four are separate
   implementations; all six read the same export.

OpenAI's configuration turns nanoda off (`"enable_nanoda": false`); our
paranoid mode includes it.

```python
mo.md(load_evidence())
```

Output:

```text
<span class="markdown prose dark:prose-invert contents"><span class="paragraph">This project has no record of a run from main yet. The record will be <code>evidence/openai-049.json</code> in this project, and this cell will show it.</span></span>
```

**Reproducing the exports.** The CI repository and the image are private,
so neither the run nor the image can be opened from outside. The source
and the toolchain are public:

1. Install Lean v4.35.0 (`elan toolchain install leanprover/lean4:v4.35.0`)
   and make a Lake project that requires Mathlib v4.35.0 (commit
   `56a005855ea17e0b0958f73ec801ae140b0a1679`); run `lake exe cache get`.
   Set `LEAN_PATH` to the output of `lake env printenv LEAN_PATH` with
   the `build/` directory of steps 3 and 4 added.
2. Download the files in `lean/` from OpenAI's commit and compare each
   SHA-256 with `LEAN_FILES` in this notebook's setup cell.
3. Copy `ComparatorChallenges/AbhyankarSathaye.lean` to
   `Challenge.lean`, build it with
   `lean -o build/Challenge.olean Challenge.lean`, and export it with the constants the comparator
   exports, in this order:
   `leanexport Challenge -- Quot Quot.mk Quot.lift Quot.ind
   OAI.AbhyankarSathaye.exists_noncoordinate_polynomial propext
   Classical.choice Quot.sound Nat.add Nat.sub Nat.mul Nat.pow Nat.gcd
   Nat.div Nat.mod Nat.beq Nat.ble Nat.land Nat.lor Nat.xor
   Nat.shiftLeft Nat.shiftRight String.ofList Char.ofNat List
   eagerReduce Nat String String.mk Char optParam autoParam
   semiOutParam outParam`.
4. Build the proof's modules with `-DautoImplicit=false`, in the order
   the accordions above list them, into `build/`; then build a
   `Solution.lean` that imports
   `OAI.AlgebraicGeometry.AbhyankarSathaye.Counterexample` and export
   it with the same constants.
5. Compare the SHA-256 of both exports with the table above, once a
   run is recorded there. `leanexport` and `lake comparator` come with
   the Lean v4.35.0 toolchain. To judge them yourself, write a configuration
   with `challenge_module` `Challenge`, `solution_module` `Solution`,
   the theorem in `theorem_names` and the three axioms in
   `permitted_axioms`, and run `lake comparator --config` on it with
   `--challenge-from-export` and `--solution-from-export`, and again
   with `--paranoid` for the six kernels.

Nobody has yet compared these hashes with exports made outside the
image. Until someone does, a hash that differs points to a difference in
the environment first, not in the proof.

**An earlier run.** Before the proof-check workflow existed, a one-off run on
27 Oct 2026 (run 40517420641, in ScienceHub's CI repository, which is
private) built the same files in ScienceHub's Lean image with digest
`sha256:6088835cad94bf6a0b098129d65182f13ae62ffd57bf31676505de221372ef6f`,
with Lean v4.35.0 (commit `eb6cafb`) and Mathlib v4.35.0 (commit
`56a0058`). It fetched each file from OpenAI's commit and compared it
with pinned SHA-256 sums, the same ones this notebook's setup cell
lists, before building. All 15 modules built with no warnings; the
challenge's one warning is its `sorry`.
`#print axioms` listed `propext`, `Classical.choice` and `Quot.sound`.
The comparator accepted the proof in default mode in 13.1 s, and in
paranoid mode all six kernels accepted it in 41.3 s. In that run the
build and the comparator shared one container with no network access,
and the comparator's own sandbox was switched off, so it printed
"WARNING: Sandbox disabled, this run is not trustworthy." That run
therefore did not separate building the proof from judging it. The
image is not public yet.

#### What this does and does not establish

An accepted run, provided the proof's build could not influence the
judge, says that the Lean statement shown above, read with Mathlib
v4.35.0's definitions, is proved in Lean's logic using no axiom beyond
`propext`, `Quot.sound` and `Classical.choice`, and, in paranoid mode,
that six kernels accept the proof. It says nothing about the preprints'
prose (cited under References): their arguments, their history of the
problem and their wider claims are not what Lean read. The second
preprint, according to OpenAI's notes, concerns a different polynomial
of degree five and the stable coordinate conjecture; its Lean result is
a separate one, not shown here.

Whether the formal statement is a faithful rendering of the
Abhyankar–Sathaye question is for you to judge from the statement
itself. OpenAI's catalogue of its formalizations,
`lean/formalization.yaml` in openai/math, gives the review status of the
collection as `unchecked` and names the method that produced them as
`agent`. Nobody at ScienceHub has yet had an algebraist read this
statement. If you are one, and you find a gap between the Lean and the
mathematics, please open a discussion on this project.

The exact-arithmetic cell above checks values at points you choose. It
confirms that $P$ is a critical point with $F(P) = -1$; it does not
show that the zero fibre is affine space.

#### References

**Sources.** The Lean files and both preprints are by OpenAI, from
[github.com/openai/math](https://github.com/openai/math) at commit
`7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a`, under the Apache License
2.0. OpenAI's own summary of what the files cover is `lean/docs/049.md`
in that repository, which also covers two related results.

```bibtex
@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}
}

@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}
}
```

**Background.** S. S. Abhyankar and T. T. Moh, Embeddings of the line in
the plane, *J. Reine Angew. Math.* 276 (1975) 148–166,
doi:10.1515/crll.1975.276.148. M. Suzuki, Propriétés topologiques des
polynômes de deux variables complexes, et automorphismes algébriques de
l'espace $\mathbb C^2$, *J. Math. Soc. Japan* 26 (1974) 241–257,
doi:10.2969/jmsj/02620241. H. Kraft, Challenging problems on affine
$n$-space, Séminaire Bourbaki 802, *Astérisque* 237 (1996) 295–317.
V. Shpilrain and J.-T. Yu, Embeddings of hypersurfaces in affine spaces,
*J. Algebra* 239 (2001) 161–173, doi:10.1006/jabr.2000.8677, on the
critical locus as an obstruction.

**This notebook.** Text and code by the ScienceHub team, Apache 2.0,
except the quoted challenge file and the Lean source, which are
OpenAI's and are reproduced unchanged.

Some outputs were cut short. The page shows them whole.

## Files

- [evidence/openai-049.json](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/evidence/openai-049.json) (16 kB)
- [lean/ComparatorChallenges/AbhyankarSathaye.json](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/ComparatorChallenges/AbhyankarSathaye.json) (366 B)
- [lean/ComparatorChallenges/AbhyankarSathaye.lean](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/ComparatorChallenges/AbhyankarSathaye.lean) (724 B)
- [lean/LICENSE](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/LICENSE) (11 kB)
- [lean/NOTICE](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/NOTICE) (621 B)
- [lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Counterexample.lean](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Counterexample.lean) (2.2 kB)
- [lean/OAI/AlgebraicGeometry/AbhyankarSathaye/CriticalPoint.lean](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/OAI/AlgebraicGeometry/AbhyankarSathaye/CriticalPoint.lean) (2.1 kB)
- [lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Fiber.lean](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Fiber.lean) (2.4 kB)
- [lean/OAI/AlgebraicGeometry/AbhyankarSathaye/FiberFormulas.lean](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/OAI/AlgebraicGeometry/AbhyankarSathaye/FiberFormulas.lean) (5.1 kB)
- [lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Identities.lean](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Identities.lean) (1.9 kB)
- [lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Lifting.lean](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Lifting.lean) (6.4 kB)
- [lean/OAI/AlgebraicGeometry/AbhyankarSathaye/LiftingIdentities.lean](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/OAI/AlgebraicGeometry/AbhyankarSathaye/LiftingIdentities.lean) (3.5 kB)
- [lean/OAI/AlgebraicGeometry/AbhyankarSathaye/LinearElimination.lean](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/OAI/AlgebraicGeometry/AbhyankarSathaye/LinearElimination.lean) (2.4 kB)
- [lean/OAI/AlgebraicGeometry/AbhyankarSathaye/LinearPresentation.lean](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/OAI/AlgebraicGeometry/AbhyankarSathaye/LinearPresentation.lean) (6.2 kB)
- [lean/OAI/AlgebraicGeometry/AbhyankarSathaye/NonCoordinate.lean](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/OAI/AlgebraicGeometry/AbhyankarSathaye/NonCoordinate.lean) (2.0 kB)
- [lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Plane.lean](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Plane.lean) (4.7 kB)
- [lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Presentation.lean](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Presentation.lean) (5.4 kB)
- [lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Quotient.lean](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Quotient.lean) (3.1 kB)
- [lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Reconstruction.lean](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Reconstruction.lean) (3.7 kB)
- [lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Stabilization.lean](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/lean/OAI/AlgebraicGeometry/AbhyankarSathaye/Stabilization.lean) (4.8 kB)
- [README.md](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/raw/README.md) (1.9 kB)

## Functions

Load them in Python with `sciencehub.load("sciencehub-team/noncoordinate-polynomial")`.

- `Dual`: A number a + b·ε with ε² = 0. Evaluating a polynomial at x + ε gives its derivative at x in b, exactly.
- `S(h, u, v, w)`: The quotient (x² + y³)/h, as \`S\` in Identities.lean.
- `P(x, y, s)`: The correction term p, as \`P\` in Identities.lean. Not the critical point P of the text.
- `construction(h, u, v, w) -> dict`: x, y, s, p and F at one point, in the order of Identities.lean.
- `gradient(point) -> list`: The four partial derivatives of F at a point, exact over the rationals.
- `load_evidence(path: Path = EVIDENCE) -> str`: The record of a Lean proof check run as Markdown, or a sentence saying why there is none to show.
- `scrub(text: str) -> str`: Text from a run record with the owner of ScienceHub's CI repository and image replaced by OWNER.
- `plural(count: int, word: str) -> str`
- `finished(stamp: str) -> str`: An ISO time as a date like 28 Oct 2026.
- `image_digest(image) -> str`: The image's digest alone, from a record that gives a digest or, in its first format, a full reference.
- `evidence_summary(evidence: dict) -> str`: The record as Markdown. It names the run by number and the image by digest only.

## Versions

- [ver_01M64BGYNQ9T7DCWA1RWRH3TFY](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/history/ver_01M64BGYNQ9T7DCWA1RWRH3TFY), 29 Oct 2026: Added README.md (current)
- [ver_01M64BEP5NC8ST4F79XW5GTY09](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/history/ver_01M64BEP5NC8ST4F79XW5GTY09), 29 Oct 2026: Added 2 files
- [ver_01M64AWH0S18AXP5FBSCP35A62](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/history/ver_01M64AWH0S18AXP5FBSCP35A62), 29 Oct 2026: Added 2 files
- [ver_01M64AWGRMCSQ0XK1M61PTFAVB](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/history/ver_01M64AWGRMCSQ0XK1M61PTFAVB), 29 Oct 2026: Added 2 files
- [ver_01M64AJ82EY41E6QT3Z2KFK0MW](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/history/ver_01M64AJ82EY41E6QT3Z2KFK0MW), 29 Oct 2026: Added 15 files
- [ver_01M64A8T523TNFZX3NV7J0CAW0](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/history/ver_01M64A8T523TNFZX3NV7J0CAW0), 29 Oct 2026: Added evidence/openai-049.json
- [ver_01M64A65SV2GW25DD9D983RN47](https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial/history/ver_01M64A65SV2GW25DD9D983RN47), 29 Oct 2026: Created

## Cite

ScienceHub. (2026). noncoordinate-polynomial \[Computer software\]. ScienceHub. https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial

```bibtex
@software{noncoordinate_polynomial_2026,
  author = {{ScienceHub}},
  title = {noncoordinate-polynomial},
  year = {2026},
  publisher = {ScienceHub},
  url = {https://sciencehub.sh/sciencehub-team/noncoordinate-polynomial}
}
```