Generally speaking, if there's a step that isn't clearly logically justified in your proof, the proof is considered wrong. So in most "normal" proof systems, t

Generally speaking, if there's a step that isn't clearly logically justified in your proof, the proof is considered wrong. So in most "normal" proof systems, this wouldn't really be a valid technique (that is, the moment someone tried to formalize it they'd run into this roadblock, and if it wasn't trivial to surmount the original proof would be thrown out). That said, there are some sequent calculi where you can do a lot of work in each step, so it might be really hard to figure out whether the step was valid; but I believe cut elimination theorems in those calculi basically assert that you can turn any valid "large step" into a (possibly very long, but finite) sequence of "small steps". From a sociological perspective, since most mathematicians don't use formal methods for most of their proofs, there can of course be proofs that may be right, but that nobody can understand well enough to verify. The ongoing famous example here is that of Shinichi Mochizuki: http://www.nature.com/news/the-biggest-mystery-in-mathematics-shinichi-mochizuki-and-the-impenetrable-proof-1.18509?WT.mc_id=TWT_NatureNew http://www.nature.com/news/the-biggest-mystery-in-mathematic.... Anyway, neither of these seem too relevant to P vs. NP.