(“A few lines where incompressibility meets unprovability”)
The Kolmogorov Complexity $K(x)$ of a string $x$ relative to an Universal Turing machine $U$ is the length of the shortest program $p$ that “prints” $x$:
$$K(x) = min\{ |p| \mid U(p) = x \}$$
A string $x$ is incompressible if $K(x) \geq |x|$. Assuming a binary alphabet $\Sigma = \{0,1\}$, for each $n \geq 1$, there are $2^n$ strings of length $n$, but there are only $2^n-1$ programs shorter than $n$, so there is at least one incompressible string among them. And it follows immediately that there are infinite incompressible strings (they exist …).
Can we catch some of them? … No! Indeed if we are reasoning in a formal theory $T$ that is powerful enough to formalize Turing machines and the notion of compressibility – e.g. Peano Arithmetic – we have:
Theorem 1: There exists $n$ such that for all strings $x$ such that $|x| \geq n$ the statement “$K(x) \geq |x|$” (i.e. $x$ is incompressible) is unprovable in $T$.
Proof: Suppose that there are infinitely many strings $x$ such that there is a proof of “$K(x) \geq |x|$”. We can build a program $p$ that enumerates all valid proofs of $T$ and whenever it founds a proof of “$K(x_i) \geq |x_i|$” for some $x_i$, it compares $|x_i|$ with $|p|$ (by the recursion theorem we can build a program that knows its length), and if $|p| < |x_i|$ then $p$ halts and prints $x_i$. So $T$ proves that $x_i$ is incompressible, but we can actually build a program shorter than $|x_i|$ which prints $x_i$, a contradiction.
Note that Theorem 1 is not provable in $T$ ! … we need $T + Con(T)$ to prove it, because no powerful enough theory can prove its own consistency or prove that some sentence is unprovable.