I apologize if this is a trivial or well known observation.

Note. This post not about the length of proofs but about their
Kolmogorov complexity.

Argument

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 the 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 a
complexity greater than $|t|$. To me this seems a bit strange. 

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

If all this is true, the very lengthy proofs that sometimes are needed
are necessarily very regular, structured, and compressible
(synonymous).