It is mentioned in Sipser's text that the complement of SAT is in $IP$, before $IP$ is formally introduced. After looking at the definition and some of the results, I still don't see why this is the case.
Is this supposed to be seen directly? Or is it easier to show that it is in $NPSPACE$, which would prove the claim since $IP = PSPACE = NPSPACE$?
This is of course a consequence of $coNP \subset PH \subset PSPACE = IP$. But it can also be proven directly for UNSAT.
The basic idea is reducing the problem to zero-testing a sum over a polynomial in a suitable finite field. It's a bit too technical to repeat neatly here, but I can give you an informal idea of how it is done.
Let's consider a formula $\phi$, define $p_\phi$ to be the polynomial where you think of $x_i$s as variables, replacing $\neg x_i$ by $(1 - x_i)$, each $\wedge$ by $\times$ and each $\vee$ by $+$. Notice that the formula is unsatisfiable iff $p_\phi(x_1, \dots, x_n) = 0$ for all $x \in \{0, 1\}^n$ or equiavalently if
$$ \sum_{x_1 \in \{0, 1\}}\sum_{x_2 \in \{0, 1\}} \dots \sum_{x_n \in \{0, 1\}} p(x_1, x_2, \dots, x_n) = 0 $$
This follows from the fact that $p_\phi \geq 0$ for any $0/1$ assignement.
The interaction is essentially the prover trying to convince the verifier that the sum is indeed zero. The interaction is done on the sum above modulo a suitable prime to keep computations manageable for the verifier. The full details are explained here. The main proof that you need to follow and convince yourself of, is that the prover cannot fool the verifier with large probability.
