Is Kolmogorov complexity (KC) relevant for proof theory? [closed]

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

closed as unclear what you're asking by Ricardo Andrade, Noah Schweber, Stefan Kohl, Andrey Rekalo, Qiaochu YuanJan 25 '14 at 0:17

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

• The technical part is correct, but I disagree with the interpretation. The fact that a proof can be (in principle) found by exhaustive search does not make it in any way regular or structured. – Emil Jeřábek Jan 24 '14 at 13:24
• This is why people don't use Kolmogorov complexity to measure proof length: it's not very meaningful to compress a proof of the classification of finite simple groups all the way down to essentially saying "it's the shortest proof of the classification of finite simple groups". I wouldn't interpret Kolmogorov complexity as "bits of inspiration", though, since almost all these bits are just stating the theorem and describing the formal proof system. All you need is one bit of inspiration: if you know there is a proof, then you can definitely find it by brute force if you search long enough. – Henry Cohn Jan 24 '14 at 13:55
• What exactly is the question here? (Also, Henry's comment is spot-on.) – Noah Schweber Jan 24 '14 at 18:37
• Would you say that the digits of $\pi$ are "very regular, structured, and compressible"? After all, the first $n$ digits of $\pi$ have Kolmogorov complexity at most $\log(n) + c$. I guess they compress pretty well, but they don't look regular to me... Perhaps what makes your thesis unsatisfying is that you don't measure the other resources required to run the program that finds the proof. – Sam Nead Jan 24 '14 at 19:31
• I think a better measure for proof theory would actually be time and space complexity, in the computational sense. In the KC sense, a description of just $k$ bits can produce a $BB(k)$-length string (busy beaver function). So perhaps there is "order", but it is very hard to work with. On the other hand, if you can make a time-complexity statement, this may be a much more reasonable measure of regularity or simplicity. – usul Jan 25 '14 at 13:14

Of course this definition of Kolmogorov complexity makes any complexity theorist cringe: what good is a small program [for] $x$ if it takes the life of the universe to produce $x$?