# Using Kolmogorov complexity to establish proof complexity lower bounds?

The motivation for this question is the fact that most n-bit strings are incompressible. Intuitively, we can propose by analogy that most proofs for Tautologies are incompressible to polynomial size. Basically, my intuition is that some proofs are inherently random and can't be compressed.

Is there a good reference on research effort related to using Kolmogorov complexity results to establish super-polynomial lower bounds on the proof size of Tautologies?

In this Ph.D. dissertation On the Complexity of Propositional Proof Systems the Incompressibility method from Kolmogorov Complexity is used to obtain Urquhart's $\Omega(n/\log n)$ lower bound for a class of Tautologies. I wonder if there are stronger results using the Incompressibility method or other results from Kolmogorov complexity?

• Kolmogorov complexity would not seem to be useful for Tautologies. For any formal system, the lexicographically first proof that an $n$-bit formula is a tautology is in fact extremely compressible: it can be described in $n+O(1)$ bits, by specifying the formula along with a program that tries all proofs in some formal system in lexicographical order. It would make more sense to look at time-bounded versions of Kolmogorov complexity. – Ryan Williams Sep 13 '10 at 4:31
• I was not clear, I mean Kolmogorov complexity results. Question is edited. – Mohammad Al-Turkistany Sep 13 '10 at 4:43
• Ryan's comment is still appropriate, even after the edit. Unless you bound some resource, the Kolmogorov complexity of any proof is a constant (for the fixed brute-force proof enumerator) plus the size of the sentence. So this way you can't get better lower bounds than linear. – András Salamon Sep 13 '10 at 9:49
• Your question specifically asks about "super-polynomial lower bounds". Ryan's argument shows that the answer is trivially no, as the Kolmogorov complexity is at most linear. Galesi's lower bound is sublinear, let alone superpolynomial. – András Salamon Sep 13 '10 at 13:18
• @turkistany: please see meta.cstheory.stackexchange.com/questions/300/…. – Kaveh Sep 14 '10 at 1:27