[YeGoblynQueenne]

Checking, it how? I mean can you describe the mechanism? How does an LLM "check" that something is (or isn't) a counterexample? Does that involve pattern matching, formal verification or model checking, some other approach?

[akalin]

In this case, the same way I would -- calling out to SymPy.

Once you verify (with SymPy or another CAS, like Mathematica) that the given function has the claimed Jacobian determinant (which involves only taking partial derivatives and taking a determinant) and the given inputs map to the same output (which involves only evaluating polynomials with some inputs), you're done.

[YeGoblynQueenne]

Why do people on this site always barge in when someone is having an argument and move the goalposts? That's not at all what the OP said.

Besides which you have no idea whether that's how the Jacobian conjecture counterexample was verified. Nobody does because no details were released.