The interesting thing about this is that trivial errors like this cannot happen (unless there is a bug in coq itself). For instance, I imagined using a library

The interesting thing about this is that trivial errors like this cannot happen (unless there is a bug in coq itself). For instance, I imagined using a library might be something like using a certain Theorem 1, with proof given by Proof 1. Since T1 and P1 are formalized, they've been verified! So I can only think of some nontrivial mistakes: the Theorem 1 is correct, but it doesn't prove what you assume in your head T1 is saying, so that you may build some valid but tautological claims. I don't know if that's a huge concern, but in any case it could happen without proof verifiers anyway. Disclaimer: I'm not actually a mathematician and I haven't tried coq yet (although I most certainly will! seems very interesting).