We explore the relationships between the computational problem of recognizing expander graphs, and the problem of efficiently approximating proof length in the well-known system of \emph{resolution}. This program builds upon known connections between graph expansion and resolution lower bounds. A proof system $P$ is \emph{(quasi-)automatizable} if there is a search algorithm which finds a $P$-proof of a given formula $f$ in time (quasi)polynomial in the length of a shortest $P$-proof of $f$. It is open whether resolution is (quasi-)automatizable. We prove several conditional non-automatizability results for resolution modulo new conjectures concerning the complexity of identifying bipartite expander graphs. Our reductions use a natural family of formulas and exploit the well-known relationships between expansion and length of resolution proofs. Our hardness assumptions are unsupported; we survey known results as progress towards establishing their plausibility. The major contribution is a conditional hardness result for the quasi-automatizability of resolution.

We explore the relationships between the computational problem of recognizing expander graphs, and the problem of efficiently approximating proof length in the well-known system of \emph{resolution}. This program builds upon known connections between graph expansion and resolution lower bounds. A proof system $P$ is \emph{(quasi-)automatizable} if there is a search algorithm which finds a $P$-proof of a given formula $f$ in time (quasi)polynomial in the length of a shortest $P$-proof of $f$. It is open whether resolution is (quasi-)automatizable. We prove several conditional non-automatizability results for resolution modulo new conjectures concerning the complexity of identifying bipartite expander graphs. Our reductions use a natural family of formulas and exploit the well-known relationships between expansion and length of resolution proofs. Our hardness assumptions are unsupported; we survey known results as progress towards establishing their plausibility. The major contribution is a conditional hardness result for the quasi-automatizability of resolution.