Using proof assistants for this purpose is certainly possible in principle, but I suspect it would take more effort than most folks who write such proofs would be interested in putting in. It would require a substantial amount of effort from the author of a purported P vs NP proof to formalize their proof.
Translating a proof written for humans into a format that a proof assistant can verify was tedious and time-consuming. I have seen estimates of between a day to a week of effort per page of human-written proof. Then, one must also formalize all prior results that the proof is building on. When we look at recent attempts at proving P vs NP, they typically use a lot of advanced machinery and sophisticated pre-existing results from prior papers, which would need to be formalized too.
Because of this, I expect it would be completely impractical to formalize both the proposed new proof and the proofs of all prior results that it relies upon, for the kinds of purported proofs we've seen so far. As user21820 points out, what would be more practical would be to formalize only the statement of all prior results that are relied upon, but not their proof. Thus, instead of proving the theorem $T$, we'd formalize a proof that $(X \land Y \land \cdots) \implies T$, where $X,Y,\dots$ are the prior results that the proof relies upon. This falls short of fully verifying the NP-completeness result, but if people have faith in the prior results, it would allow people to gain confidence in the new result. This would be a lot more realistic than formalizing the entire proof of $T$: while it would take some effort to formalize all of the prior results $X,Y,\dots$, it's a lot less than the effort to formalize the proofs of those prior results too.
Still, it would be challenging and require a non-trivial expenditure of effort to formalize a proof, even with this trick.
You can look at existing libraries of theorems in mathematics and computer science that have been formalized and formally verified: see http://us.metamath.org/ and http://formalmath.org/ and https://www.isa-afp.org/topics.html and http://mizar.org/library/. You might notice that a lot of what is formalized there concerns basic undergraduate material. We're a far way from formalizing all theorems taught at an undergraduate level, let alone those taught at a graduate level, let alone new research results.
For more background, see https://math.stackexchange.com/q/792010/14578 and https://math.stackexchange.com/q/113316/14578 and https://math.stackexchange.com/q/1767070/14578 and https://math.stackexchange.com/q/2747661/14578 and http://www.ams.org/notices/200811/tx081101370p.pdf.