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).

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).

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).

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).