sciencehub-team/noncoordinate-polynomialPublic

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.