Algebraic geometry · Conjecture
Must every polynomial map F: → ℂⁿ with a constant nonzero Jacobian determinant have a polynomial inverse?
Earlier version 8 of this page. View current →
The cited explicit three-variable witness refutes the universal complex formulation. Its determinant and colliding rational inputs are exposed as separate, inspectable evidence.
Precise statement
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.
Figures and explorable examples. Selecting a statement opens its exact wording.
Visual setup
The conjecture asks the same question in every dimension n. It fails from three up and is still open in two variables.
Reading boundary. A failure in one dimension says nothing about lower ones: the two-variable question is untouched by the higher-dimensional maps.
Dimension n
Has a polynomial inverse?
✗ Fails there: counterexamples exist? OpenDashed: proposed, not yet establishedEach cell links to its statement and status
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
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.
Each input maps to (−1/4, 0, 0) under F, and det JF = −2 everywhere.
Universal conjecture; one non-injective map in dimension three suffices to refute it.
Conjecture · Primary formulation
DisprovedULAM research manuscript 2026Constant Jacobian implies a polynomial inverse
Universal conjecture; one non-injective map in dimension three suffices to refute it.
A concrete failure of injectivity and hence of a polynomial inverse.
Theorem · Counterexample
ProvedGao 2026A 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.
Extends the three-variable failure to every higher dimension.
Theorem · Counterexample
ProposedGao 2026Counterexamples in every dimension from three up
A family of counterexamples in every dimension above two; shown as proposed until checked beyond the preprint.
Extends the three-variable failure to every higher dimension. Shown as proposed: the preprint has no recorded formal or independent check beyond its own exact computations.
The source leaves this dimension open; the three-variable witness cannot be specialized to refute it.
Conjecture · Different statement · related variant
OpenThe two-variable Jacobian question
The source leaves this dimension open; the three-variable witness cannot be specialized to refute it.
The source witnesses this existence statement using the three-variable counterexample.
Theorem · Supporting result
Provedalerad/alpoge-lean project 2026No polynomial inverse for the three-variable witness
The source witnesses this existence statement using the three-variable counterexample. Analytic derivative correspondence and further geometric interpretations are outside this formal result.
Three variables over the rationals, also viewed over the complexes. This witness does not settle the two-variable question.
A constant determinant with three inputs sharing an output →Three-variable counterexample related to Two-variable question.
VariantDimensions 3 and 2. The three-variable witness settles the universal formulation, while the two-variable restriction remains a different question.
Limit A collision in ℂ³ supplies no counterexample in ℂ².
Independent relationship review: not recorded. Link to this connection
Assuming Three-variable counterexampleProved
Local invertibility does not guarantee a global inverse
Under stated assumptionsA constant nonzero Jacobian can coexist with several inputs having the same output, invalidating the universal polynomial-inverse conclusion.
Limit The remaining two-variable question requires its own argument.
Supporting statements
Source-grounded explanation · independent explanation review: pending.
How the problem is attacked, and what each line of attack cannot yet reach.
The counterexample can be inspected through exact polynomial differentiation and substitution of three rational inputs.
Cannot yet reach A determinant calculation alone would not demonstrate failure of global inversion.
Supporting statements
Source-grounded explanation · independent explanation review: pending.
Shuhong Gao analyzes the counterexample and its algebraic structure.
This is a separate contribution, not the original discovery.
A public Lean revision proves the determinant, fiber collision and failure of polynomial inversion.
A source build report is not an OpenMath execution; analytic identification is outside the formal scope.
The cited manuscript records Alpöge’s announcement, Mathew’s question and Fable’s contribution to finding the displayed witness.
Credits concern discovery; independent OpenMath mathematical review is pending.
The classical question asks whether a constant nonzero polynomial Jacobian forces global polynomial invertibility.
The question depends on the field and dimension.
| Literature | Status OpenMath assessment · Oct 13, 2026.
|
|---|---|
| Formal | 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. |
| Computation | |
| Review | 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 Collection last checked Oct 13, 2026. |
Complete formal proof reported externally
The polynomial witness is source-reported complete; OpenMath has not built it. The project also proves jacobian_det and not_injective.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Alpoge.three_point_fiberCommit b8eec94711a9b73151929b78cbd7cb999a008590
Complete formal proof reported externally
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
Alpoge.FormalConjecturesJC.jacobian_conjecture_falseCommit b8eec94711a9b73151929b78cbd7cb999a008590
External proof reports do not establish an OpenMath run, independent statement correspondence, or independent mathematical review.
Choose a starting point below. Each result links to its exact statement, cited passages and checks.
Read the setting and notation before comparing the results.
Read the mathematical argument; inspect its statement for assessment and scope.
Inspect the formal statement, assumptions and reported checks.
ULAM research manuscript (no author named) · Preprint · Jul 20, 2026
Explicit map and verification of determinant and fiber
Shuhong Gao · Preprint · Jul 31, 2026
Introduction and analysis of the counterexample
alerad/alpoge-lean project · Project documentation · Jul 23, 2026
README trust boundary; Alpoge/Basic.lean and Alpoge/FormalConjectures.lean
Formalization
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
Selected literature; source observations and coverage limits are retained in the publication details.
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.
ULAM research manuscript (no author named)
The manuscript cites Levent Alpöge’s announcement, credits Akhil Mathew for asking the question and Fable for the work leading to the example. No named author is printed on this verification manuscript; these discovery credits are not its bibliographic authorship.
Shuhong Gao
No AI contribution is asserted by this source record.
alerad/alpoge-lean project
The project reports an AI-assisted formalization and computer-algebra workflow; this is distinct from the original discovery.
These are source credits; they do not imply OpenMath accounts, endorsements or independent mathematical review.