Comment by zarzavat

As the recent "proof" of the Collatz conjecture shows, that's not enough in an adversarial context. Human mathematicians don't submit proofs that take advantage of soundness bugs in Lean. AIs do.