Jacobian conjecture

Overview

Known

The cited explicit three-variable witness refutes the universal complex formulation. Its determinant and colliding rational inputs are exposed as separate, inspectable evidence.

Constant Jacobian implies a polynomial inverseDisprovedAlpöge 2026
A constant determinant with three inputs sharing an outputProvedGao 2026

Latest

Separate algebraic analysisJul 31, 2026
Polynomial counterexample formalizedJul 23, 2026

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.

Background

The explicit map has no polynomial inverseProved

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.

Inspect the counterexample● Proved under stated assumptions

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.
A constant determinant with three inputs sharing an output →

Sources & review

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.

On a counterexample to the Jacobian conjectureIntroduction and analysis of the counterexamplePreprintOriginal passage ↗
Alpöge counterexample in LeanREADME trust boundary; Alpoge/Basic.lean and Alpoge/FormalConjectures.leanProject documentationOriginal passage ↗
An explicit Jacobian counterexampleExplicit map and verification of determinant and fiberPreprintOriginal passage ↗

Results

The question 2

Variants and analogues 1

Open
The two-variable Jacobian question
The source leaves this dimension open; the three-variable witness cannot be specialized to refute it.
Conjecture · Different statement · related variant
Open
The two-variable Jacobian question
Every polynomial map F: ℂ² → ℂ² with constant nonzero Jacobian determinant has a polynomial inverse.
Assumptions
- Exactly two complex variables.
In this problem
The source leaves this dimension open; the three-variable witness cannot be specialized to refute it.
Sources
- On a counterexample to the Jacobian conjecture →
Open statement page →

Background 1

Proved
The explicit map has no polynomial inverse
A formal algebraic counterexample. Identification with analytic Fréchet derivatives and further geometric interpretations are outside the claimed formalization.
alerad/alpoge-lean project 2026Formalized
Theorem · Supporting result
Provedalerad/alpoge-lean project 2026
The explicit map has no polynomial inverse
For the displayed three-variable map F over ℚ, there are no polynomial tuples defining a two-sided compositional inverse; the mirrored universal Jacobian conjecture statement is false.
Assumptions
- Polynomial Jacobian and composition over ℚ.
In this problem
A formal algebraic counterexample. Identification with analytic Fréchet derivatives and further geometric interpretations are outside the claimed formalization.
Formal proofs
- Lean: failure of the recorded polynomial-inverse assertion ↗Complete formal proof reported externally
Sources
- Alpöge counterexample in Lean →
Open statement page →

Connections

Consequences 1

Assuming A constant determinant with three inputs sharing an outputProved

Local invertibility does not guarantee a global inverse
Under stated assumptions
A 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.
- The explicit map has no polynomial inverseProved
Sources & review
Supporting statements
- A constant determinant with three inputs sharing an output →
- The explicit map has no polynomial inverse →
- An explicit Jacobian counterexample ↗Explicit map and verification of determinant and fiber
- On a counterexample to the Jacobian conjecture ↗Introduction and analysis of the counterexample
- Alpöge counterexample in Lean ↗README trust boundary; Alpoge/Basic.lean and Alpoge/FormalConjectures.lean
Source-grounded explanation · independent explanation review: pending.

Approaches

How the problem is attacked, and what each line of attack cannot yet reach.

Check a witness instead of a universal obstruction

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.

A constant determinant with three inputs sharing an output (Proved)

Sources & review

Supporting statements

A constant determinant with three inputs sharing an output →

An explicit Jacobian counterexample ↗Explicit map and verification of determinant and fiber
Alpöge counterexample in Lean ↗README trust boundary; Alpoge/Basic.lean and Alpoge/FormalConjectures.lean

Source-grounded explanation · independent explanation review: pending.

Timeline

Jul 31, 2026Separate algebraic analysisAssessment
Shuhong Gao analyzes the counterexample and its algebraic structure.
This is a separate contribution, not the original discovery.
- A constant determinant with three inputs sharing an outputProved
- On a counterexample to the Jacobian conjecture ↗Introduction and analysis of the counterexample
Jul 23, 2026Polynomial counterexample formalizedFormalization
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.
- A constant determinant with three inputs sharing an outputProved
- The explicit map has no polynomial inverseProved
- Alpöge counterexample in Lean ↗README trust boundary; Alpoge/Basic.lean and Alpoge/FormalConjectures.lean
Jul 19, 2026Jacobian conjecture in dimension threeCounterexample
An explicit map in C^3 with det JF=-2 and three different points having the same image; padding gives higher-dimensional counterexamples.
Open the Frontier report →
Jul 2026Explicit three-variable counterexampleProposal
Levent Alpöge’s reported collaboration with Claude Fable 5 produced the displayed algebraic witness.
Credits concern discovery; independent OpenMath mathematical review is pending.
- A constant determinant with three inputs sharing an outputProved
- An explicit Jacobian counterexample ↗Explicit map and verification of determinant and fiber
1939Keller’s global invertibility questionFoundation
The classical question asks whether a constant nonzero polynomial Jacobian forces global polynomial invertibility.
The question depends on the field and dimension.
- Constant Jacobian implies a polynomial inverseDisproved
- On a counterexample to the Jacobian conjecture ↗Introduction and analysis of the counterexample

Full history with sources →

Evidence

Evidence by kind
Literature	2 preprints · 1 project Status OpenMath assessment · Oct 13, 2026. Disproved: An explicit Jacobian counterexample · Explicit three-variable counterexample ↗ · source date not recorded · checked Oct 13, 2026The all-dimensions complex Jacobian conjecture.
Formal	2 complete proofs 2 formalizations below ↓ 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	None recorded
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.

Formalizations

A constant determinant with three inputs sharing an output →

Lean: the three-point fiberComplete formal proof reported externally

Open formal source ↗

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

Declaration & revision

Alpoge.three_point_fiber

Commit b8eec94711a9b73151929b78cbd7cb999a008590

The explicit map has no polynomial inverse →

Lean: failure of the recorded polynomial-inverse assertionComplete formal proof reported externally

Open formal source ↗

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

Declaration & revision

Alpoge.FormalConjecturesJC.jacobian_conjecture_false

Commit b8eec94711a9b73151929b78cbd7cb999a008590

Alpöge counterexample in Lean: README trust boundary; Alpoge/Basic.lean and Alpoge/FormalConjectures.lean →

External proof reports do not establish an OpenMath run, independent statement correspondence, or independent mathematical review.

Sources

Choose a starting point below. Each result links to its exact statement, cited passages and checks.

Start here

Introduction: Jacobian conjecture →

Bibliography 3

An explicit Jacobian counterexample →
Levent Alpöge · Preprint · Jul 2026
Explicit map and verification of determinant and fiber
On a counterexample to the Jacobian conjecture →
Shuhong Gao · Preprint · Jul 31, 2026
Introduction and analysis of the counterexample
Alpöge counterexample in Lean →
alerad/alpoge-lean project · Project documentation · Jul 23, 2026
README trust boundary; Alpoge/Basic.lean and Alpoge/FormalConjectures.lean

Research activity · 1 entry

Contributions

Discovery: Levent Alpöge with Claude Fable 5. 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

Alpöge counterexample in Lean · sources & artifacts →

Selected literature; source observations and coverage limits are retained in the publication details.

Record details

Record version: 1
Classification: MSC2020 14R15 / 14R10
Prerequisite level: graduate

Source observations & version history →

Overview

Known

Latest

Background

Landscape

Check the counterexample

Three inputs, one image

A constant determinant with three inputs sharing an output

Results

The question 2

Assumptions

In this problem

Sources

Assumptions

In this problem

Formal proofs

Sources

Variants and analogues 1

Assumptions

In this problem

Sources

Background 1

Assumptions

In this problem

Formal proofs

Sources

Connections

Consequences 1

Approaches

Check a witness instead of a universal obstruction

Timeline

Evidence

Formalizations

A constant determinant with three inputs sharing an output →

The explicit map has no polynomial inverse →

Sources

Start here

Bibliography 3

Contributions

Formal algebraic evidence