The cited explicit three-variable witness refutes the universal complex formulation. Its determinant and colliding rational inputs are exposed as separate, inspectable evidence.
Complex polynomial maps in finite dimension n ≥ 1. A local derivative condition is being compared with global polynomial invertibility; the two-variable restriction is a separate question.
Question paraphrased by OpenMath. Original wording is available in the sources.
Landscape
Figures and explorable examples. Selecting a statement opens its exact wording.
Check the counterexample
Exact rational arithmetic: the three inputs have the same image, and the Jacobian determinant is the constant −2. A polynomial inverse would make F injective, so none exists.
Input (x, y, z)
F(x, y, z)
det JF there
(0, 0, −1/4)
(−1/4, 0, 0)
−2
(1, −3/2, 13/2)
(−1/4, 0, 0)
−2
(−1, 3/2, 13/2)
(−1/4, 0, 0)
−2
All (x, y, z)
—
−2 (expands to a constant)
This checks the stated witness by direct computation. It says nothing about two variables, where the question is open.
Visual setup
Three inputs, one image
The displayed rational points have the same image under the explicit map F. Segments indicate mapping, not paths in ℂ³.
Reading boundary. The layout is symbolic; it is not a projection of the six-real-dimensional domain. It says nothing about the two-variable case.
Select a statement below for its scope and evidence. The text view describes the complete drawing.
Text version
Three input points (0,0,−1/4), (1,−3/2,13/2) and (−1,3/2,13/2) map to (−1/4,0,0), despite det JF = −2.
Coordinates in the drawing are illustrative unless the caption specifies an exact example.
Inspect the counterexample
●Proved
A constant determinant with three inputs sharing an output
A concrete failure of injectivity and hence of a polynomial inverse. The coordinate degrees are 7, 6 and 4; a cubic fiber relation does not make this a cubic coordinate map.
Authored by OpenMath source curation on 2026-10-13 (AI-assisted curation). Independent review of this visual explanation is pending; linked assertions and relationships have their own assessments.
A concrete failure of injectivity and hence of a polynomial inverse.
Gao 2026Formalized
Theorem · Counterexample
●ProvedGao 2026
A constant determinant with three inputs sharing an output
Set s=xy and u=1+s. The map F(x,y,z)=u3z+y2u(4+3s)y+3xu2z+3xy2(4+3s)2x−3x2y−x3z has detJF=−2. The distinct inputs (0,0,−1/4), (1,−3/2,13/2) and (−1,3/2,13/2) all map to (−1/4,0,0).
Assumptions
Use the displayed map over a characteristic-zero field.
In this problem
A concrete failure of injectivity and hence of a polynomial inverse. The coordinate degrees are 7, 6 and 4; a cubic fiber relation does not make this a cubic coordinate map.
The source witnesses this existence statement using the three-variable counterexample.
alerad/alpoge-lean project 2026Formalized
Theorem · Supporting result
●Provedalerad/alpoge-lean project 2026
No polynomial inverse for the three-variable witness
There exists a polynomial map F: Q3 → Q3 with constant Jacobian determinant −2 and no two-sided polynomial compositional inverse.
Assumptions
Polynomial maps and composition are taken over ℚ.
In this problem
The source witnesses this existence statement using the three-variable counterexample. Analytic derivative correspondence and further geometric interpretations are outside this formal result.
Reported in sources: Formal polynomial determinant, fiber collision and no-inverse results have public pinned Lean sources. Analytic derivative correspondence is outside their stated scope; no local proof build is recorded.
CComputation
None recorded
RReview
Not yet reviewed
OpenMath assessment: The cited explicit three-variable witness refutes the universal complex formulation. Its determinant and colliding rational inputs are exposed as separate, inspectable evidence.
Source comparison and page curation only; independent mathematical review is pending.
OpenMath pilot collection · OpenMath source curation · assessed Oct 13, 2026 · review due Jan 13, 2027
The endpoint witnesses the statement over ℚ with three variables. The explicit rational points also give the complex non-injectivity; analytic correspondence was not formalized by this project.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
README trust boundary; Alpoge/Basic.lean and Alpoge/FormalConjectures.lean
Research activity · 1 entry
Contributions
The discovery report credits Levent Alpöge, Akhil Mathew for asking the question and Fable for work leading to the example. The July 20 ULAM verification manuscript prints no author name. Separate analysis: Shuhong Gao. Formalization: the alerad/alpoge-lean project’s reported AI-assisted workflow.
Formalization
Formal algebraic evidence
The pinned Lean project supplies separately inspectable determinant, collision and no-inverse statements.
No OpenMath build or independent proof adjudication has been performed.
Related statements · context, not additional proved progress