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

By "every theorem $t$ has a proof with low Kolmogorov complexity", we mean:

every theorem $t$ has a proof $p$ with $K(p)\leq K(t)+c\leq|t|+c$ where $c$ is a constant.
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, 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, and compressible (synonymous).