An Independent Lean 4 Verification of the
Alpöge–Fable Counterexample
to the Jacobian Conjecture

§1Background and the Conjecture

The Jacobian Conjecture, posed by O.-H. Keller in 1939, asserts:

The conjecture remained open for over 85 years, resisting attacks across algebraic geometry, analysis, and combinatorics. It was known to be true for $n = 1$ (trivially), and for $n = 2$ it remained one of the central open problems in polynomial maps. It was also known to be stably equivalent to a family of related conjectures in noncommutative algebra (Dixmier, Poisson).

In 2025, Levent Alpöge and an AI collaborator (Claude Fable 5) found an explicit counterexample in dimension $n = 3$, disproving the conjecture at $n \geq 3$. The present paper formalizes that counterexample in Lean 4.

§2The Counterexample

2.1 The map

The counterexample is the polynomial map $F = (F_1, F_2, F_3) : \mathbb{C}^3 \to \mathbb{C}^3$. Using coordinates $(x, y, z)$ with $x = X_0,\, y = X_1,\, z = X_2$:

This map is polynomial in $x, y, z$ with rational (in fact integer) coefficients. It therefore lifts to a map over $\mathbb{Q}$, which is what the Lean formalization uses — a sufficient domain since the injectivity failure we need to exhibit is rational.

2.2 The Jacobian determinant

The Jacobian matrix is: $$\text{Jac}\, F = \begin{pmatrix} \partial F_1/\partial x & \partial F_1/\partial y & \partial F_1/\partial z \\ \partial F_2/\partial x & \partial F_2/\partial y & \partial F_2/\partial z \\ \partial F_3/\partial x & \partial F_3/\partial y & \partial F_3/\partial z \end{pmatrix}$$

Its determinant is computed symbolically — no numerical approximation — in the Lean formalization using MvPolynomial.pderiv over ℚ. The computation expands to a large polynomial, then the kernel confirms it equals the constant $-2$.

2.3 The collision

The three preimages differ in their $y$- and $z$-coordinates. All three are rational, so the collision is verified by exact arithmetic over $\mathbb{Q}$.

§3Lean 4 Formalization

3.1 Setup

The formalization uses Mathlib4. The map components are defined as elements of MvPolynomial (Fin 3) ℚ — multivariate polynomials in three variables over the rationals. Variables are named X 0, X 1, X 2 (corresponding to $x$, $y$, $z$).

3.2 The polynomial components

3.3 The Jacobian matrix

3.4 The three theorems

3.5 Axiom check

After lake build, running:

returns exactly:

No sorryAx. The three axioms listed are Lean 4's standard logical foundations — propositional extensionality, classical choice, and quotient soundness — present in every Mathlib proof. The verification is kernel-clean.

3.6 A technical note on map_ofNat

During formalization, a subtlety arose: the simp call for the Jacobian determinant must separate the map_ofNat normalization into its own prior simp only pass. Combining it with the pderiv_* lemmas in a single simp call produces a looping rewrite that times out. The isolated pass is therefore:

This ordering is a Lean 4 / Mathlib4 artifact, not a mathematical subtlety.

§4Consequences and Scope

4.1 What the result settles

The Jacobian Conjecture is false for $n = 3$ (and hence for all $n \geq 3$ by embedding). The question for $n = 2$ — whether a polynomial map $\mathbb{C}^2 \to \mathbb{C}^2$ with constant nonzero Jacobian must be an automorphism — remains open.

4.2 Relation to the Dixmier and Poisson conjectures

The Jacobian Conjecture (JC), the Dixmier Conjecture (DC), and the Poisson Conjecture (PC) are stably equivalent: $\text{JC}_{2n} \Leftrightarrow \text{DC}_n$ and $\text{DC}_n \Leftrightarrow \text{PC}_n$ (Tsuchimoto 2005, Belov-Kanel–Kontsevich 2007).

4.3 Epistemic ledger

§5File Availability

The Lean 4 source file JacobianCounterexample.lean is available at the Zenodo deposit:

To run: clone the deposit, ensure Mathlib4 is available (lake update), then lake build. The expected output ends with zero errors, zero warnings. The axiom check can be run interactively in any Lean 4 environment.

§ RefReferences