sciencehub-team/noncoordinate-polynomialPublic

# /// 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")

with app.setup:
    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",
    }


@app.class_definition
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


@app.function
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


@app.function
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


@app.function
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}


@app.function
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


@app.function
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."


@app.function
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)


@app.function
def plural(count: int, word: str) -> str:
    return f"{count} {word}" + ("" if count == 1 else "s")


@app.function
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')}"


@app.function
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


@app.function
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.",
        ]
    )


@app.cell
def _():
    import marimo as mo

    return (mo,)


@app.cell(hide_code=True)
def _(mo):
    mo.md(r"""
    # 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.
    """)
    return


@app.cell(hide_code=True)
def _(mo):
    mo.md(r"""
    ## 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."
    """)
    return


@app.cell(hide_code=True)
def _(mo):
    mo.md(r"""
    ## 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.
    """)
    return


@app.cell(hide_code=True)
def _(mo):
    mo.md(r"""
    ## 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$.
    """)
    return


@app.cell(hide_code=True)
def _(mo):
    mo.md(r"""
    ## 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.
    """)
    return


@app.cell
def _(mo):
    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])
    return h_in, u_in, v_in, w_in


@app.cell
def _(h_in, mo, u_in, v_in, w_in):
    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))
    return


@app.cell(hide_code=True)
def _(mo):
    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.
    """)
    return


@app.cell
def _(mo):
    _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)
    return


@app.cell(hide_code=True)
def _(mo):
    mo.md(r"""
    ## 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.
    """)
    return


@app.cell
def _(mo):
    mo.md(load_evidence())
    return


@app.cell(hide_code=True)
def _(mo):
    mo.md(r"""
    **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.
    """)
    return


@app.cell(hide_code=True)
def _(mo):
    mo.md(r"""
    ## 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.
    """)
    return


@app.cell(hide_code=True)
def _(mo):
    mo.md(r"""
    ## 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.
    """)
    return


if __name__ == "__main__":
    app.run()