John Harrison spoke once about checking the results of some peer reviewed mathematical research: he has found bugs in the proofs and even a faulty theorem, which he corrected by giving a formal proof.
Are there examples of doing this for already formalised theorems? Definitions might be wrong, logics might be expressing something bad.
