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
sorryProof. sorry
Nobody has tried yet.