What the proof, instance, and verifier mean in the definition of NP problem? I came across a definition of NP problems:

Definition. A decision problem $X ∈ NP$, if there exists a polynomial time verifier $V$ such that For every yes instance $x ∈ X$, there exists a polysized proof y such that $V (x, y) = yes$. For every no instance $x ∈ X$, and for every proof y, we have $V (x, y) = no$.

It is very confusing, can anyone help to use an example and a counterexample to illustrate what the the proof, instance, and verifier are? Thanks in advance.
 A: In principal, they can be anything - the definition is purely abstract: a decision problem $X$ is in $NP$ if there is a polynomial-time function $V$ such that if $x\in X$, then $V(x, y)=1$ for some polysized $y$, and if $x\not\in X$, then $V(x, y)=0$ for every $y$.
In practice, and more informally, the idea is that a decision problem $X$ is in $NP$ if it can be expressed as "Is there a [thing] such that [property]?" where (a) the [thing] in question (if it exists) is small relative to the size of the input, and (b) it is easy to tell if a given [thing] has the desired [property]. For example, if a Hamiltonian path in a graph exists, it is "short" relative to the size of the graph, and telling whether some random sequence of vertices is a Hamiltonian path is an easy task.
The most subtle part of this equation in my opinion is the verifier - in the Hamiltonian path example, it is just a function $V$ such that, if $x$ is a (code for a) graph and $y$ is a (code for a) sequence of nodes in the graph, we have $V(x, y)=1$ iff $y$ is a Hamiltonian path in $x$ and $V(x, y)=0$ otherwise. Well, actually, $V$ isn't a function, strictly speaking - $V$ is a machine. So really when we claim "--- is in NP," we should precisely describe a machine $V$ which is an appropriate verifier. In the examples I'm familiar with, the verifier is never a particularly complicated machine, so we often just skip over it (e.g. "then, check whether $y$ is a Hamiltonian path in $x$"); but I believe in more sophisticated complexity theory than what I'm familiar with, we do have to be more explicit.

To motivate the definition: consider the Halting problem - "does the $e$th Turing machine halt on input $e$?" - as a decision problem. This fails to be in NP for two reasons. First, it doesn't have a verifier at all, let alone a fast one: if $V$ is any total computable function, then EITHER there is some (index for a) Turing machine $x$ which does not halt on input $x$, and some $y$, such that $V(x, y)=1$; OR there is some (index for a) Turing machine $x$ which does halt on input $x$, but such that for every $y$ we have $V(x, y)=0$. Either way, it breaks. Second, even if there were a fast verifier for the Halting problem, proofs are long: a "short" Turing machine can take for-freakin'-ever to halt. (This is actually the crucial issue behind the non-existence of verifiers.)
