Note. The title was modified. Previous title was
"Every theorem t has a proof no more complex than~|t|. Is this right?"


The question ("Is Kolmogorov complexity (KC) relevant for proof theory?") arises because every theorem has a proof with low Kolmogorov complexity". To be more specific,

*Every theorem $t$ has a proof $p$ with $K(p)\leq K(t)+c\leq|t|+c'$, where $c$ and $c'$ are constants.*  
*Proof:* It is assumed that there is a proof checking algorithm $C(x)$ that
outputs TRUE if $x$ is a correct proof, FALSE otherwise.
Then there exists a fixed (depending on the formal system) Turing 
machine $M$ with
  Input: $t$ a string (that may be a theorem)  
  - $M$ enumerates all the proofs until (and if) $t$ is proved.  
  - When $t$ is proved, print the proof $p$ and halt.  
Thus, if $t$ is a theorem, $M(t)$ prints a proof of $t$.  
Using the universal TM, we get
  $ K(p) \leq K(t) + c \leq |t| + c' $
where $c$ and $c'$ are constants.


----------


Thus, and apart from a constant, no theorem needs a proof with Kolmogorov complexity greater than $|t|$. To me this seems a bit strange. 

In other words, the number of bits of "inspiration" (or "non-deterministic bits",
or "oracle bits") needed to prove any theorem $t$ is at most $|t|+c$.

If this is true, the very lengthy proofs that sometimes are needed to prove some
simple to state theorems are necessarily very regular / structured / compressible (synonymous).