The analyzability lower-bound conjecture for propositional proof systems

Let $Q$ be a propositional proof system. A proof system is analyzable when its associated proof-analysis problem admits the efficient analysis described in the paper, and it is optimal when it simulates every propositional proof system within polynomial overhead.

Analyzability requires lower bounds. For every propositional proof system $Q$, if $Q$ is analyzable, then $Q$ is not optimal.

The claim formalizes the expectation that analysis algorithms for propositional proof systems require proof-complexity lower bounds. The paper gives Resolution as the motivating example, but does not establish the conjecture in general.