Let $\mathcal{C}$ be a complexity class and $A$ be a language. The statement ``$A \not\in \mathcal{C}$'' is a separation of $A$ from $\mathcal{C}$. A separation is constructive if there is an efficient algorithm called a refuter that prints counterexamples to the statement ``$M$ decides $A$'' for every $\mathcal{C}$-algorithm $M$. Concretely, refuters witness errors of $M$ on $A$ by printing, on input $1^n$, an $n$-bit string $x$ such that $M(x) \neq A(x)$. Many recent breakthroughs in lower bounds and derandomization, like the algorithmic method, rely on constructive separations as a core component. Chen, Jin, Santhanam, and Williams (TheoretiCS, 2024) studied the consequences of constructivizing classical non-constructive lower bounds in complexity theory. They showed that (1) constructivizing many known separations would imply breakthrough lower bounds, and (2) some separations are impossible to constructivize.

We study a more general notion of ``efficient refutation'' in terms of $\mathcal{C}$-Student-Teacher Games, where the $\mathcal{C}$-refuter (Student) is allowed to adaptively propose candidate counterexamples $x_i$ to an omniscient Teacher. If $x_i$ fails to witness an error, Teacher reveals a counterexample $y_i$ to the statement ``$x_i$ is a counterexample to the statement `$M$ decides $A$' '' --- the nature of $y_i$ depending on how the separated language $A$ and complexity class $\mathcal{C}$ are defined. We show:

--- If there is a P-Student-Teacher constructive separation of Palindromes from one-tape nondeterministic $O(n^{1 + \varepsilon})$ time (Maass 1984), then $\text{NP} \not\subset \text{SIZE}[n^k]$ for every $k$.
--- If there is a uniform $\text{AC}^0[\text{qpoly}]$-Student-Teacher protocol generating truth tables of super fixed polynomial circuit complexity, then $\text{P}\neq\text{NP}$.
--- There is no $\text{P}$-Student-Teacher protocol which for infinitely many $c>0$, generates high-$\text{K}^{n^c}$ strings.

Our results imply a conditional separation of Je\v r\'abek's theory $\text{VAPC}$ from $\text{V}^1$, a theory equivalent to Buss's theory $\text{S}^1_2$. This improves and significantly simplifies the work of Ilango, Li, and Williams (STOC 2023), who separate $\text{VAPC}$ from the weaker theory $\text{VPV}$ under the existence of indistinguishability obfuscation. We do not use cryptographic assumptions in our separation. Instead we introduce a natural and plausible conjecture on the uniformity of proofs in bounded arithmetic, inspired by Kreisel's Conjecture in logic. We believe this conjecture to be of independent interest.

Submitted an older version of the paper.

Let $\mathcal{C}$ be a complexity class and $A$ be a language. The statement ``$A \not\in \mathcal{C}$'' is a separation of $A$ from $\mathcal{C}$. A separation is constructive if there is an efficient algorithm called a refuter that prints counterexamples to the statement ``$M$ decides $A$'' for every $\mathcal{C}$-algorithm $M$. Concretely, refuters witness errors of $M$ on $A$ by printing, on input $1^n$, an $n$-bit string $x$ such that $M(x) \neq A(x)$. Many recent breakthroughs in lower bounds and derandomization, like the algorithmic method, rely on constructive separations as a core component. Chen, Jin, Santhanam, and Williams (TheoretiCS, 2024) studied the consequences of constructivizing classical non-constructive lower bounds in complexity theory. They showed that (1) constructivizing many known separations would imply breakthrough lower bounds, and (2) some separations are impossible to constructivize.

We study a more general notion of ``efficient refutation'' in terms of $\mathcal{C}$-Student-Teacher Games, where the $\mathcal{C}$-refuter (Student) is allowed to adaptively propose candidate counterexamples $x_i$ to an omniscient Teacher. If $x_i$ fails to witness an error, Teacher reveals a counterexample $y_i$ to the statement ``$x_i$ is a counterexample to the statement `$M$ decides $A$' '' --- the nature of $y_i$ depending on how the separated language $A$ and complexity class $\mathcal{C}$ are defined. We show:

--- If there is a P-Student-Teacher constructive separation of Palindromes from one-tape nondeterministic $O(n^{1 + \varepsilon})$ time (Maass 1984), then $\text{NP} \not\subset \text{SIZE}[n^k]$ for every $k$.
--- If there is a uniform $\text{AC}^0[\text{qpoly}]$-Student-Teacher protocol generating truth tables of super fixed polynomial circuit complexity, then $\text{P}\neq\text{NP}$.
--- There is no $\text{P}$-Student-Teacher protocol which for infinitely many $c>0$, generates high-$\text{K}^{n^c}$ strings.

Our results imply a conditional separation of Je\v r\'abek's theory $\text{VAPC}$ from $\text{V}^1$, a theory equivalent to Buss's theory $\text{S}^1_2$. This improves and significantly simplifies the work of Ilango, Li, and Williams (STOC 2023), who separate $\text{VAPC}$ from the weaker theory $\text{VPV}$ under the existence of indistinguishability obfuscation. We do not use cryptographic assumptions in our separation. Instead we introduce a natural and plausible conjecture on the uniformity of proofs in bounded arithmetic, inspired by Kreisel's Conjecture in logic. We believe this conjecture to be of independent interest.