How hard would it be to state P vs. NP in a proof assistant?
I'm going to disagree with DW. I think that it is possible (although difficult) for a P vs. NP result to be stated in a proof assistant, and moreover, I wouldn't trust any supposed proofs unless they were formalized in this way, unless they came from very reputable sources.
In particular, none of the resources DW states are based on type theory, which is a very promising direction for proof assistants. Coq has been used to formalize the proof of the 4-color theorem among others, so it's clearly capable of some heavy mathematical lifting.
To answer your specific questions:

The main reason is that theorem provers aren't widely accepted in the mathematical community. Learning them takes effort, and mathematicians are often skeptical of the underlying techniques (type theory, constructive math, etc.)
But there are some fields where leading researchers are very comfortable with making large developments formalized in a proof assistant, like category theory, programming language theory, formal logic, etc. So I think there is as much of a cultural issue as an inherent feasibility issue.
The other reason is that, so far, most of the purported &quot;proofs&quot; have been by cranks, who don't want to formalize their result because it will inevitably reveal the flaws.

It is not hard at all to state P vs. NP in a proof assistant. One could use Turing Machines, but it would probably be easier to model a simple Turing-complete programming language using inductive families to model small-step semantics, and define the run-time as the number of steps a program takes. You could define $P$ as the languages accepted by programs halting in a polynomial number of steps, and $NP$ as languages that can be verified in polytime with a polynomial-length certificate.
EDIT: It turns out there are existing techniques for showing that algorithms run in polynomial time in a theorem prover. So this could be used either to show a polytime algorithm for an NP-hard problem, or to derive a contradiction from the existence of such an algorithm.

There is tons of software that is capable of verifying such a proof, provided the proof was written using that software. The two candidates I'd put the most stock in are Coq and Lean. Coq in particular has been used to verify several major results in mathematics.