Counterexample to the Jacobian conjecture in dimension three

Fabbrev

Alpöge's counterexample: a self-map of k³ with Jacobian determinant -2 that is not injective.

noncomputable abbrev F : RegularFunction k (Fin 3) (Fin 3) :=
  ![(1 + 𝑋 * 𝑌)^3 * 𝑍 + 𝑌^2 * (1 + 𝑋 * 𝑌) * (4 + 3 * 𝑋 * 𝑌),
    𝑌 + 3 * 𝑋 * (1 + 𝑋 * 𝑌)^2 * 𝑍 + 3 * 𝑋 * 𝑌^2 * (4 + 3 * 𝑋 * 𝑌),
    2 * 𝑋 - 3 * 𝑋^2 * 𝑌 - 𝑋^3 * 𝑍]

Gabbrev

A variant with Jacobian determinant 1, which works in every characteristic.

noncomputable abbrev G : RegularFunction k (Fin 3) (Fin 3) :=
  ![(1 + 2 * 𝑋 * 𝑌)^3 * 𝑍 + 4 * 𝑌^2 * (1 + 2 * 𝑋 * 𝑌) * (2 + 3 * (𝑋 * 𝑌)),
    𝑌 + 3 * 𝑋 * (1 + 2 * 𝑋 * 𝑌)^2 * 𝑍 + 12 * 𝑋 * 𝑌^2 * (2 + 3 * (𝑋 * 𝑌)),
    -𝑋 + 3 * 𝑋^2 * 𝑌 + 𝑋^3 * 𝑍]

det_jacobian_Gtheorem

theorem det_jacobian_G : (G k).Jacobian.det = 1 := by
  simp only [G, Jacobian, ← map_ofNat (C : k →+* MvPolynomial (Fin 3) k), Matrix.det_fin_three,
    Matrix.of_apply, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two,
    Matrix.head_cons, Matrix.tail_cons, map_add, map_neg, Derivation.map_one_eq_zero, pderiv_mul,
    pderiv_pow, pderiv_C, pderiv_X_self, pderiv_X_of_ne, ne_eq, Fin.reduceEq, not_false_eq_true]
  simp only [map_ofNat]
  ring

aeval_G_eqtheorem

G identifies the two distinct points (1, 0, 1) and (0, 3, -71).

theorem aeval_G_eq : (G k).aeval ![1, 0, (1 : k)] = (G k).aeval ![0, 3, -71] := by
  funext i
  fin_cases i <;> simp [RegularFunction.aeval]; grind

Builds on

import Conjectura.Vendor.JacobianCounterexample · maintainer — open · raw source

Vendored for Conjectura from formal-conjectures (Google DeepMind), formalised by Paul Lezeau. Released under Apache 2.0.

Copyright (c) 2025 The Formal Conjectures Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Formal Conjectures Authors

Full credits