A new approach to defining complexity of propositional formulas and proofs is suggested. Instead of measuring the size of these syntactical structures in the propositional language, the article suggests to define the complexity by the size of external descriptions of such constructions. The main result is a lower bound on proof complexity with respect to this new definition of complexity.

We study from the proof complexity perspective the proof search problem : •Is there an optimal way to search for propositional proofs?We note that, as a consequence of Levin’s universal search, 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 without restricting 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 information-efficiency function $i_P$ assigning to a tautology a natural number, and we show that: • $i_P$ characterizes time any P-proof search algorithm has to use on $\tau $,•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$.We isolate and motivate the problem to establish unconditional super-logarithmic lower bounds for $i_P$ 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. (shrink)