<p>I know one can show that by <span class="math-container">$\mathsf{coNP}\subseteq\mathsf{NEXP}=\mathsf{MIP}$</span>. But here I would like to start with a <span class="math-container">$\mathsf{coNP}$</span>-complete problem and show there is a two-prover one-round interactive proof system for it.</p>
<p>I read Luca Trevisan's <a href="https://lucatrevisan.github.io/pcp/lecture01.pdf" rel="nofollow noreferrer">lecture note</a>, which says that it was once conjectured that <span class="math-container">$\mathsf{coNP}\not\subseteq\mathsf{MIP}$</span>, but it turned out Babai, Fortnow and Lund showed <span class="math-container">$\mathsf{MIP}=\mathsf{NEXP}$</span>. Also <span class="math-container">$\mathsf{coNP}$</span> does not have a constant-round interactive proof system unless the polynomial hierarchy collapses. So perhaps the question is not totally trivial, at least to me.</p>

CC BY-SA 4.0
2023-06-13T06:51:03.243Z
Do you have any reason to believe this is easier than the general MIP = NEXP result?
Emil Jeřábek
CC BY-SA 4.0
2023-06-13T17:44:05.813Z
Thanks for asking. That's exactly what I'm wondering. I would like to get intuition on why $\mathsf{coNP}\subseteq\mathsf{MIP}$ without knowing $\mathsf{MIP}=\mathsf{NEXP}$.
user50394
CC BY-SA 4.0
2023-06-14T17:21:52.753Z
You can look at the SUMCHECK protocol---which shows that #P (and in particular coNP) is in IP---without reading the MIP = NEXP paper. It'd be interesting if multiple provers make this easier though (i.e., if coNP in MIP is easier than coNP in IP).
Huck Bennett
<cc.complexity-theory><complexity-classes><nexp>
How do we show directly coNP is in MIP?
user50394
# How do we show directly coNP is in MIP?

(Asked by: username_0 on 2023-06-12)

I know one can show that by $\mathsf{coNP}\subseteq\mathsf{NEXP}=\mathsf{MIP}$. But here I would like to start with a $\mathsf{coNP}$-complete problem and show there is a two-prover one-round interactive proof system for it.

I read Luca Trevisan's [lecture note](https://lucatrevisan.github.io/pcp/lecture01.pdf), which says that it was once conjectured that $\mathsf{coNP}\not\subseteq\mathsf{MIP}$, but it turned out Babai, Fortnow and Lund showed $\mathsf{MIP}=\mathsf{NEXP}$. Also $\mathsf{coNP}$ does not have a constant-round interactive proof system unless the polynomial hierarchy collapses. So perhaps the question is not totally trivial, at least to me.

**Tags:** cc.complexity-theory, complexity-classes, nexp
> **Comments:**
> **username_1**: Do you have any reason to believe this is easier than the general MIP = NEXP result?  
> **username_0**: Thanks for asking. That's exactly what I'm wondering. I would like to get intuition on why $\mathsf{coNP}\subseteq\mathsf{MIP}$ without knowing $\mathsf{MIP}=\mathsf{NEXP}$.  
> **username_2**: You can look at the SUMCHECK protocol---which shows that #P (and in particular coNP) is in IP---without reading the MIP = NEXP paper. It'd be interesting if multiple provers make this easier though (i.e., if coNP in MIP is easier than coNP in IP).  

---

## 0 answers

