# A polynomial that cuts out affine space but is not a coordinate OpenAI's Lean statement and proof that for every n ≥ 4 there is a complex polynomial F in n variables with ℂ[x₁, …, xₙ]/(F) ≅ ℂ[y₁, …, yₙ₋₁] that is not a coordinate. The three-variable case is not covered. OpenAI's preprint claims this answers the Abhyankar–Sathaye question in the negative for n ≥ 4. Nobody at ScienceHub has yet had an algebraist read the Lean statement against the conjecture, and OpenAI's catalogue marks its formalizations as unchecked. The notebook explains the statement and the construction, lets a reader evaluate F at its critical point, shows the Lean source, and says which runs of Lean's comparator exist and what they show. | File | What it holds | | ---------------------------------------------- | -------------------------------------------------------------------------------- | | `lean/ComparatorChallenges/` | OpenAI's challenge: the statement with `sorry`, and the comparator configuration | | `lean/OAI/AlgebraicGeometry/AbhyankarSathaye/` | The 15 files of the proof | | `lean/LICENSE` | The Apache License 2.0, as OpenAI ships it | | `lean/NOTICE` | Where the files come from and what changed (nothing) | | `evidence/openai-049.json` | Unchanged record of main run 40886152492, accepted under gVisor | - **Source:** https://github.com/openai/math, commit `7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a`, directory `lean/`. - **Terms:** Apache License 2.0. The notebook's own text and code are by the ScienceHub team, also Apache 2.0.
SHA-256 7489bba69fccc9c60576d2274105cb544389557e649775176a299ded0afa2b19