Just wondering, why do people not use Coq/Isabelle/Agda/etc in order to check such proofs? Wouldn't that save them from the "shame" of producing yet-another-incorrect P(!)=NP proof?
Because that's an extremely large amount of work to do, even if you're already familiar with the tools.
It wouldn't be quite so bad if there were a huge repository of already proven theorems you could pull from. But in reality you'll probably find yourself defining what a Turing machine is, what asymptotic complexity is, deriving results like the master theorem, and a thousand other trivialities you would just skip over in a paper.
It is especially problematic that there isn't a common repository of reference implementations of well-known unproved propositions. It would be so easy to make a subtle mistake in your definitions that allowed an existence proof to go through in a way that wouldn't generalize to the actual definition. For example, when you define probabilistic computation, if you declare that a probabilistic gate is a stochastic matrix with real number entries, you will incorrectly find that there exists probabilistic programs that solve the halting problem.
> It wouldn't be quite so bad if there were a huge repository of already proven theorems you could pull from.
What about things like Metamath [1]? (Not sure if there is a more mature similar effort, Metamath is just the one I've heard of.) It seems like it has quite a lot of the "thousand other trivialiaties" you mentioned, but maybe it's still not enough to make a real dent?