Comment by pcloadlett3r

A counterexample (at least the jacobian conjecture one) is a lot easier to manually verify than 10MB Lean proof