I just fed this to GPT 5.6 Sol:

  Counterexample to Jacobian conjecture:

  ((1+xy)^3 z + y^2 (1+xy) (4+3xy), y + 3 x (1+xy)^2 z + 3 x y^2 (4+3xy), 2 x - 3 x^2 y - x^3 z): \C^3\to \C^3, has jacobian determinant -2, and sends (0, 0, -1/4), (1, -3/2, 13/2), and (-1, 3/2, 13/2) to (-1/4, 0, 0)

GPT wrote some SymPy code to check it. The response?

"As written, this is an explicit counterexample to the Jacobian conjecture. I checked it using exact symbolic algebra.

I do not see an algebraic catch in what you typed. Unless a term or exponent differs from the intended expression, it appears to disprove the conjecture. This deserves serious independent checking rather than casual dismissal."

Waiting for someone to write the Lean proof.