Wikipedia · research solved · AMS 14

hardknown result, no worker yet

Jacobian conjecture

Theorem · jacobian_conjecture

The **Jacobian Conjecture**: any regular function (i.e. vector valued polynomial function from) kⁿ → kᵐ whose Jacobian is a non-zero constant has an inverse that is given by a regular function, where k is a field of characteristic 0.

This is false: F has Jacobian determinant 1 but identifies two distinct points, so it admits no inverse. This counterexample works in all characteristics.

Formal statement · Lean 4.lean
theorem jacobian_conjecture {k : Type} [CommRing k] [Nontrivial k] :
    answer(False) ↔ ∀ {σ : Type} [Fintype σ] [DecidableEq σ], JacobianConjectureProp k σ := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗