  We study from the proof complexity perspective the (informal) proof search
problem:
  Is there an optimal way to search for propositional proofs?
  We note that for any fixed proof system there exists a time-optimal proof
search algorithm. Using classical proof complexity results about reflection
principles we prove that a time-optimal proof search algorithm exists w.r.t.
all proof systems iff a p-optimal proof system exists.
  To characterize precisely the time proof search algorithms need for
individual formulas we introduce a new proof complexity measure based on
algorithmic information concepts. In particular, to a proof system $P$ we
attach {\bf information-efficiency function} $i_P(\tau)$ assigning to a
tautology a natural number, and we show that:
  - $i_P(\tau)$ characterizes time any $P$-proof search algorithm has to use on
$\tau$ and that for a fixed $P$ there is such an information-optimal algorithm,
  - a proof system is information-efficiency optimal iff it is p-optimal,
  - for non-automatizable systems $P$ there are formulas $\tau$ with short
proofs but having large information measure $i_P(\tau)$.
  We isolate and motivate the problem to establish {\em unconditional}
super-logarithmic lower bounds for $i_P(\tau)$ where no super-polynomial size
lower bounds are known. We also point out connections of the new measure with
some topics in proof complexity other than proof search.
