An explicit noncoordinate polynomial with affine three-space zero fibre

Formalization

• OpenAI math release, Lean scope note 049: A stable-coordinate counterexample in four variables (release Lean docs, October 2026). Describes the formalized scope, including a noncoordinate F in ℂ[x_1,…,x_n] with quotient ≅ ℂ^[n-1] for every n ≥ 4, a companion statement on n−1 commuting locally nilpotent derivations, and the degree-five stable noncoordinate, with links to the three Comparator challenges; the three-variable case is not covered. [family-level]
• OpenAI math release, AbhyankarSathaye.lean (comparator statement) (openai/math, October 2026). Lean statement OAI.AbhyankarSathaye.exists_noncoordinate_polynomial matching Corollary 1.2 (every n ≥ 4); the proof field in this statement file is sorry.
• OpenAI math release, StableCoordinateFour.lean (comparator statement) (openai/math, added in the 7 October 2026 update). Lean statement for the degree-five example of the 5 October companion paper, which strengthens this paper's zero-fibre result to all fibres; the proof field in this statement file is sorry. [family-level]

Related prior literature mentioned by others

• Shulim Kaliman, Stéphane Vénéreau and Mikhail Zaidenberg, Simple birational extensions of the polynomial ring C^[3] (arXiv:math/0104204v2, 2001). Math Referee's source assessment discusses Theorem 4.2(a) as background for the manuscript's restricted affirmative embedding results and separates that context from the internal construction; this work is already in the manuscript's bibliography.

Possibly relevant literature (found by the agent, not checked)

• Drew Lewis, Venereau-type polynomials as potential counterexamples (arXiv:1007.2230; J. Pure Appl. Algebra 217 (2013)). Discusses Vénéreau-type polynomials as candidate counterexamples to the Abhyankar–Sathaye embedding conjecture, the conjecture this paper's Theorem 1.1 addresses in four variables.
• Shulim Kaliman and Mikhail Zaidenberg, Venereau polynomials and related fiber bundles (arXiv:math/0308191, 2003). Earlier four-variable candidates with affine three-space fibres, connected in its abstract to the Abhyankar–Sathaye embedding problem.
• Vladimir L. Popov, Around the Abhyankar–Sathaye conjecture (arXiv:1409.6330, 2014). Paper on the conjecture and on commuting locally nilpotent derivations, relevant both to Theorem 1.1 and to the derivation-theoretic interpretation via D = h∂_u − 3u²∂_v + 2u∂_w.
• Parnashree Ghosh and Neena Gupta, On the triviality of a family of linear hyperplanes (arXiv:2206.15210, 2022/2023). Affirmative Abhyankar–Sathaye results for linear hyperplanes x_1^{r_1}⋯x_m^{r_m}y = F, complementing the affirmative results by Ghosh–Gupta–Pal and Ghosh cited in the introduction.

Digests and expositions

• AI Proved What?, One variable too few? A stable coordinate that is not a coordinate (episode 049, October 2026). This AI-assisted video and transcript explain both constructions, outline the October paper's filtration and derivation obstruction, and distinguish it from the September paper's critical-point argument. [AI-generated per source] [family-level]
• Math Referee, An explicit noncoordinate polynomial with affine three-space zero fibre — panel review (review, 2026-10-13). This AI-generated review reports no demonstrated error in four completed model assessments of the manuscript, records coverage qualifications and source checks, and states that human assessment remains pending. [AI-generated per source]
• Math Referee, Optional AI source assessment — noncoordinate polynomial (source assessment, 2026-10-13). This separate AI assessment details checks of the lifting lemma, quotient presentation, critical point and inverse maps, with reproducible symbolic calculations and explicit limits on its bibliography and formalization coverage. [AI-generated per source]

News and blogs

• Curtis Pyke, One OpenAI Math Proof Target Passed Twice. Two Hit Our Memory Cap. (Kingy AI, 2026-10-06). The post reports two successful local Comparator checks of OAI.AbhyankarSathaye.exists_noncoordinate_polynomial, provides public logs, and states that Codex operated the checks without human mathematical review of correspondence between the formal statement and manuscript.