# How do we show directly coNP is in MIP?

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, 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.

• Do you have any reason to believe this is easier than the general MIP = NEXP result? Jun 13, 2023 at 6:51
• 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}$. Jun 13, 2023 at 17:44
• 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). Jun 14, 2023 at 17:21