MIP = NEXP

Equivalence · BFL90, FRS88

Statement

The class of languages with multi-prover interactive proofs equals NEXP; two provers and polynomially many rounds suffice. $\mathbf{NEXP}\subseteq \mathbf{MIP}$ — BFL90 — and $\mathbf{MIP}\subseteq \mathbf{NEXP}$, since a multi-prover proof system is equivalent to a probabilistic verifier with oracle access to a fixed proof, which an exponential-time nondeterministic machine can guess — FRS88.

Sketch

For $\mathbf{NEXP}\subseteq \mathbf{MIP}$, BFL90 reduce to an oracle-3SAT instance, arithmetize it as a low-degree polynomial identity over a large field, and check the identity by a sum-check protocol with one prover. The second prover is queried at a random point to force the first to answer according to a single multilinear function, which a multilinearity test checks — BFL90.

Notes

• The single-prover analogue is IP = PSPACE — Sha90; scaling NEXP ⊆ MIP down to $\mathbf{NP}$ led to the PCP theorem — standard.
• With entangled provers the class grows: $\mathbf{NEEXP}\subseteq {\mathbf{MIP}}^{\ast }$ — NW19 — and ${\mathbf{MIP}}^{\ast }=\mathbf{RE}$ — JNVWY20; see MIP* versus MIP.