Agreed! But I think in the case of the abc conjecture, verifying that the conjecture was stated correctly in Lean wouldn…

Agreed! But I think in the case of the abc conjecture, verifying that the conjecture was stated correctly in Lean wouldn't be that hard. Not nearly as hard as the amount of effort the community put into trying to understand the purported proof.