For a complexity class C and language L, a constructive separation of L \notin C gives an efficient algorithm (also called a refuter) to find counterexamples (bad inputs) for every C-algorithm attempting to decide L. We study the questions: Which lower bounds can be made constructive? What are the consequences ... more >>>

We establish an equivalence between two algorithmic tasks: *derandomization*, the deterministic simulation of probabilistic algorithms; and *refutation*, the deterministic construction of inputs on which a given probabilistic algorithm fails to compute a certain hard function.

We prove that refuting low-space probabilistic streaming algorithms that try to compute functions f\in\mathcal{FP} ... more >>>

This paper studies the \emph{refuter} problems, a family of decision-tree \mathrm{TFNP} problems capturing the metamathematical difficulty of proving proof complexity lower bounds. Suppose \varphi is a hard tautology that does not admit any length-s proof in some proof system P. In the corresponding refuter problem, we are given (query ... more >>>