Each formal system can be encoded in a binary string. For instance, you can use the input string that a pre-specified Turing machine needs in order to enumerate all the theorems in a theory in the output string. Thus the input string is actually a compressed version of a string that enumerates all the theorems of the theory in some order. Please let me know if I am right up to here.
Now let us take two theories that have the same proof theoretic strength (I am aware that there are several possible definitions of this, but I hope this fact will not change the answer much). Question: Should we expect that the strings that code these two theories have the same Kolmogorov complexity? I am not sure why I expect that this should be the case.