IP = PSPACE

General proof sketch:

   1. We consider the language \(\#SAT_D<\math> which is the decision variant of <math>\#SAT\), the language of CNF formulae and their satisfying assignment. 
   
   \( \#SAT_D = \{\langle \phi, K\rangle: \text{ K is the number of satisfying assignments of }\phi\} \)
   
   where \(\phi\) is a 3CNF formula. Prove that \(\#SAT_D \in \mathsf{IP}\) via arithmetization and the sumcheck protocol.
   
   2.   Arithmetization is the idea of converting boolean formulae to an algebraic form. So, \(x\land y\) can be represented by \(x\cdot y\) and \(\neg x\) can be represented by \(1-x\) and \(x\lor y\) can be represented by \(1 - (1- x)(1-y)\).
   
   3. Sumcheck protocol: add general description of the sumcheck protocol
   
   4. Using a very similar idea we then prove that \(\mathsf{TQBF} \in \mathsf{IP}\) and since \(\mathsf{TQBF}\) is \(\mathsf{PSPACE}\)-complete, we have that \(\mathsf{PSPACE} \in \mathsf{IP}\). 
   
   5. And we know that \(\mathsf{IP} \in \mathsf{PSPACE}\) by the following argument. We know that the prover can use an arbitrary function, it can in principle use unbounded computational power. Therefore, given any verifier, the optimum prover strategy can be computed using \(poly(|x|)\) and \(2^{poly(\abs{x})}\) time. This is by brute forcing through the possible space of prover verifier communication, optimizing for the probability of acceptance by the verifier. This takes polynomial space, hence \(\mathsf{IP} \in \mathsf{PSPACE}\).