Agreed; translating to Lean/Coq is more likely to prove the positive rather than the negative. It may still be useful in pinpointing where incorrect proofs go wrong.