A kernel-checked verification of the Jacobian-conjecture counterexample

Independent formal verification, in Lean 4 + mathlib, of the two central algebraic claims of the counterexample announced 2026-07-20 by Levent Alpöge (crediting Akhil Mathew and the Fable model) — preprint "A Counterexample to the Jacobian Conjecture", Theorem 3.1.

The map F = (P, Q, R) : 𝔸³ → 𝔸³, exactly as published:

P = (1 + xy)³·z + y²·(1 + xy)·(4 + 3xy)
Q = y + 3x·(1 + xy)²·z + 3x·y²·(4 + 3xy)
R = 2x − 3x²·y − x³·z

What is verified (fully kernel-checked; no sorry, no native_decide)

• Keller.jacobian_det — the formal Jacobian determinant det (∂Fᵢ/∂xⱼ) = −2 as an identity in MvPolynomial (Fin 3) ℚ (formal pderiv partials through Matrix.det_fin_three) — hence valid over every field of characteristic zero, all coefficients being rational.
• Keller.eval_point0/1/2, Keller.points_pairwise_distinct — the full three-point fiber of the preprint's Theorem 3.1: F(0, 0, −1/4) = F(1, −3/2, 13/2) = F(−1, 3/2, 13/2) = (−1/4, 0, 0), with the three points pairwise distinct.
• Keller.keller_not_injective, Keller.keller_not_injective_C — non-injectivity of the induced maps on ℚ³ and on ℂ³.
• Keller.jacobian_conjecture_counterexample — the headline conjunction: constant nonzero formal Jacobian ∧ not injective, i.e. a Keller map that is not a polynomial automorphism: the Jacobian conjecture fails in dimension 3.

Axioms: every theorem depends on exactly [propext, Classical.choice, Quot.sound] — verify with #print axioms Keller.jacobian_conjecture_counterexample.

What is NOT verified here

The preprint's global-geometry sections (the incidence variety, fiber classification), the properness/behaviour-at-infinity analysis, and the stabilization to dimensions n > 3. This artifact certifies precisely the algebraic content of Theorem 3.1.

Relation to other formalizations

Complementary to google-deepmind/formal-conjectures#4474 (P. Lezeau and reviewers), which proves a rescaled det = 1 variant valid in all characteristics. This file instead certifies the preprint's original map verbatim (det = −2) with the full three-point fiber.

Build (reproducible)

With elan installed, in this directory:

lake exe cache get   # fetch the mathlib build cache
lake build           # kernel-checks everything

Pinned: leanprover/lean4:v4.32.0-rc1; mathlib 360da6fa66c1273b76b6b2d8c5666fd5ac2e3b56.

Credits

The mathematics is due to the preprint's authors (Alpöge–Mathew–Fable, 2026-07-20). This verification: Jason Hickey (with Claude). The author thanks Katherine Schlitz for bringing the announcement to his attention. License: Apache-2.0.