# Generate string with large Kolmogrov complexity

Given $c$, can you generate a string $s$ with $K(s) \ge c$, along with a proof of that fact?

I think the answer is no except for small $c$, but I'm not sure.

Roughly, the theorem says that there exists a concrete constant $C$ (which is a function of your consistent set of axioms) for which no fixed string can be proven to have Kolmogorov complexity larger than $C$. The core idea is that if you could do it for every string, then you can write a program of size $\log n + O(1)$ to search for and eventually output strings with complexity $n$, which is a contradiction for sufficiently large $n$.