The Dixmier conjecture implies the Jacobian conjecture, and is false in dimension 3 and above

A Lean 4 proof of four statements from Google DeepMind's Formal Conjectures (pinned commit 7bdc4a42), all in FormalConjectures/Arxiv/math.0608009/DixmierConjecture.lean:

Formal Conjectures' name	What it says
dixmier_conjecture.variants.jacobian_implication	The Dixmier conjecture in dimension n implies the Jacobian conjecture in dimension n.
dixmier_conjecture.variants.dimension_ge_three	The Dixmier conjecture is false in every dimension n ≥ 3.
dixmier_conjecture.variants.dimension_three	The Dixmier conjecture is false in dimension 3.
dixmier_conjecture	The Dixmier conjecture, generalised to all dimensions, is false: it fails for some n.

The Dixmier conjecture says that, over a field of characteristic zero, every endomorphism of the n-th Weyl algebra is an automorphism. The Weyl algebra is the algebra generated by x₁, …, xₙ and y₁, …, yₙ with x_i y_i − y_i x_i = 1 and all other pairs commuting: the canonical commutation relations of quantum mechanics. Dixmier posed it in 1968 for the first Weyl algebra (Bull. Soc. Math. France 96, Problem 1).

The implication. Formal Conjectures credits it to H. Bass, E. Connell and D. Wright, "The Jacobian conjecture: reduction of degree and formal expansion of the inverse", Bull. Amer. Math. Soc. 7 (1982), and K. Adjamagbo and A. van den Essen include it in the chain of implications of their Theorem 7 (arXiv:math/0608009). The converse holds stably, by three independent proofs (Tsuchimoto 2005, Belov-Kanel and Kontsevich 2007, Bavula), which this repository does not use.

The other three statements follow from the implication, because the Jacobian conjecture fails in dimension 3 and above, and that is proved here as a Lean theorem rather than cited. Formal Conjectures' JacobianConjecture.G is a polynomial map of K³, a variant of what Formal Conjectures calls Alpöge/Fable's counterexample (L. Alpöge, 2026). Formal Conjectures proves that it has Jacobian determinant 1 and sends (1, 0, 1) and (0, 3, −71) to the same point, and from that proves the Jacobian conjecture false. This repository restates the map as DixJac.cG, proves both facts again, and pads it with identity coordinates to a counterexample in every dimension n ≥ 3 (DixJac.not_jacobianConjectureProp, in DixJac/Pad.lean).

Earlier work. The failure of the Dixmier conjecture in dimension 3 was found within days of Alpöge's counterexample, in July 2026, in An Explicit Counterexample to the Dixmier Conjecture in A3, which Teller and Naughton credit to Jeff Pickhardt and the Omniscience Research Agent (19 July), and independently by Marcus Teller, whose Lean proofs cover the determinant, the collision and the matrix identities, and Brian Naughton. William Mayner circulated a note covering every n ≥ 3. This repository proves Formal Conjectures' statements in Lean, including the implication for every n and every field of characteristic zero.

What is not claimed. Formal Conjectures marks the Dixmier conjecture in dimension 1 and dimension 2 as open, and it marks the Jacobian conjecture in dimension 2 open too. Nothing here touches them, or the converse implication.

The proof

The Weyl algebra in Formal Conjectures is a bare quotient of a free algebra, so most of the work is a small library for it.

1. Polynomials inside the Weyl algebra (DixJac/Basic.lean). Polynomials in the x's embed as a commutative subalgebra, and so do polynomials in the y's. Moving y_j past a polynomial p in the x's costs a derivative: y_j p = p y_j − ∂p/∂x_j.
2. The polynomial representation is faithful (DixJac/Faithful.lean). The Weyl algebra acts on polynomials: x_i multiplies by X_i and y_i acts as −∂/∂X_i. Every element can be written in normal order, with the x's on the left. Commuting with x_i differentiates the y-part, so by induction on degree an element acting as zero has every derivative zero; in characteristic zero it is then a constant, and that constant is zero. So the representation is faithful, and anything that commutes with every x_i is a polynomial in the x's.
3. The endomorphism (DixJac/Construction.lean). Given a polynomial map F with invertible Jacobian determinant, let A be the inverse of its Jacobian matrix. The vector fields D_i = Σ_j A_ij ∂_j satisfy D_i(F_k) = δ_ik and commute with each other: their commutator kills every F_k, and a derivation that kills every F_k is zero because the Jacobian is invertible. So x_k ↦ F_k, y_i ↦ Σ_j A_ij y_j respects the relations and defines an endomorphism of the Weyl algebra.
4. The inverse (DixJac/Main.lean). If the Dixmier conjecture holds, that endomorphism has an inverse ψ. Each ψ(x_i) commutes with every x_j, so by step 2 it is a polynomial G_i in the x's. G is then a polynomial inverse of F on both sides.
5. Dimension 3 and above (DixJac/Pad.lean, DixJac/FormalTarget.lean). The padded counterexample has a block-diagonal Jacobian with determinant 1 and still sends two points to one, so the Jacobian conjecture fails in every dimension n ≥ 3, and with step 4 so does the Dixmier conjecture.

The statements themselves are Formal Conjectures' own. Challenge.lean copies the definitions and the four statements verbatim, with only their attributes removed, and scripts/check-fc-match.py regenerates that text from Formal Conjectures at the pinned commit and requires an exact match. That compares text only: Formal Conjectures builds with Lean and Mathlib v4.33.1, this repository with Lean v4.35.0-rc3, and the script does not read what Formal Conjectures' files import. Palomar does not accept escaped name components such as «math.0608009» in theorem names, so Challenge.lean states the four theorems in the namespace DixmierConjecture with Formal Conjectures' leaf names. Solution.lean proves them under both names, and an example checks that each pair has the same statement at every universe level.

Building

Lean v4.35.0-rc3 and Mathlib 5e0c4e5239cb0a2d86d68a884bf52cfd963fce22. Formal Conjectures is not a dependency.

lake exe cache get
lake build
lake env lean audit/Axioms.lean
lake env lean audit/Control.lean
python3 scripts/check-lean-sources.py
python3 scripts/check-fc-match.py --self-test
ruby scripts/validate-formalization.rb

audit/Axioms.lean checks that the four theorems and the key lemmas use only propext, Classical.choice and Quot.sound. audit/Control.lean checks that the axiom audit catches a sorry, specialises the implication to the rationals in dimension 2, checks the commutation relation and the derivative in the representation, and checks the counterexample. The self-test runs 28 altered copies of the inputs, each of which must fail. scripts/verify-comparator.sh runs Palomar's Comparator check; it needs Linux, so it runs in CI.

Licence

Apache 2.0. The files copied from Formal Conjectures keep its copyright notice.