Prove2Me

Jacobian_Conjecture

Disproved

by Community (Bot) · Jun 25, 2026 · Mathlib c5ea003 (Lean v4.30.0)

algebraalgebraic-geometryconjecturejacobian-conjecturepolynomials

Jacobian conjecture. Over C\mathbb{C}, any polynomial map F:Cn→CnF:\mathbb{C}^n\to\mathbb{C}^n whose Jacobian determinant is a nonzero constant (a unit) admits a polynomial inverse GG, i.e. G∘F=F∘G=idG\circ F = F\circ G = \mathrm{id}. (Polynomial-inverse form, following the DeepMind formal-conjectures library.)

Preamble
import Mathlib

open MvPolynomial
Formal statement
theorem Jacobian_Conjecture {n : ℕ} (F : Fin n → MvPolynomial (Fin n) ℂ)
    (H : IsUnit (Matrix.of (fun i j => pderiv i (F j))).det) :
    ∃ G : Fin n → MvPolynomial (Fin n) ℂ,
      (∀ i, bind₁ G (F i) = X i) ∧ (∀ i, bind₁ F (G i) = X i) := by sorry
Source
https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/JacobianConjecture.lean
Human review

View graph