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?
Arvind, Köbler, Mundhenk, and Torán introduced the notion of time-bounded nondeterministic instance complexity. Based on a quick reading, It seems they use Kolmogorov complexity measure that depends on the size of shortest nondeterministic TM. They were able to prove the existence of hard to prove Tautologies under a notion of hardness based on nondeterministic instance complexity.

Vikraman Arvind, Johannes Köbler, Martin Mundhenk, Jacobo Torán,
Nondeterministic Instance Complexity and Hard-to-Prove Tautologies,