# Is there a version of MIP=NEXP with relatively efficient provers?

(My question is not a duplicate of this question.)

Fix a good coding of non-deterministic random-access machines.
For non-negative integers $m$ that code such a machine, let
$\operatorname{states}(m)$ denote the number of internal states in the coded machine.

("hc" stands for "hard-coded".)
Choose some polynomial function $hcpoly$, and let $L$ be the language
$\{\langle m\hspace{.02 in},\hspace{-0.025 in}t,\hspace{-0.02 in}s\hspace{-0.02 in}\rangle \;\; : \;\; m$ codes such a machine and $\:t\leq 2^{hcpoly(\operatorname{states}(m))}\:$ and
there is a sequence of non-deterministic choices which will make that machine
accept the empty string in at most $t$ time without using more than $s$ space$\}\;$.

Is there a MIP protocol for $L\hspace{.02 in}$ in which the provers use not
much more than $t$ time and/or not much more than $s$ space?

That could just mean $\:poly(\hspace{.02 in}\operatorname{length}(\langle m\hspace{.02 in},\hspace{-0.025 in}t,\hspace{-0.02 in}s\hspace{-0.02 in}\rangle))\:$ time and space, although
ideally it would be $\:poly(\operatorname{states}(m))\hspace{-0.03 in}\cdot \hspace{-0.03 in}t\:$ time and $\:poly(\operatorname{states}(m))\hspace{-0.03 in}+\hspace{-0.03 in}s\:$ space.

Yes. ​ ​ ​ This paper constructs "a one-round succinct MIP of knowledge, where each prover runs in time $t\cdot \operatorname{polylog}(t)$ and space $s\cdot \operatorname{polylog}(t)$ and the verifier runs in time" ​ $\operatorname{length}(m) \cdot \operatorname{polylog}(t)$ .