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