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)

"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.

Here's your Lean proof https://github.com/google-deepmind/formal-conjectures/pull/4...

...no need for any lean here

[dead]