How hard would it be to state P vs. NP in a proof assistant?


GJ Woeginger lists 116 invalid proofs of P vs. NP problem. Scott Aaronson published "Eight Signs A Claimed P≠NP Proof Is Wrong" to reduce hype each time someone attempts to settle P vs. P. Some researchers even refuse to proof-read papers settling the "P versus NP" question.

I have 3 related questions:

  1. Why are people not using proof assistants that could verify whether a proof of P vs. NP is correct?
  2. How hard or how much effort would it be to state P vs. NP in a proof assistant in the first place?
  3. Is there currently any software that would be at least in principle capable of verifying a P vs. NP proof?