[nicf]

This was definitely something I saw on HN, but for what it's worth, in my conversations that night with other mathematicians no one brought up Lean proofs or peer review even as a joke. We just copied and pasted the polynomials into a computer algebra system and checked it ourselves and then said "holy shit, I guess the Jacobian conjecture is false". Couldn't have taken more than five minutes after we first saw the tweet.

[tptacek]

Right, that's what was so funny about it. Finding a counterexample: an incredible mathematical achievement. Verifying a counterexample: barely even a weeknight homework problem in an undergraduate multivariable course.