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?