I have posted this several times about the nature of mathematical theorem's proof as being indeterminate in complexity here and elsewhere.

The main way of approaching this problem to me was to envision a proofs complexity as the size of the Kolmogorov complexity for an input value and computational process via the length of terms used in conjunction with primitives and variables associated with the theorems proof. Answers to this thought have ranged from:

"Kolmogorov complexity is somewhat different from proof complexity, but it's also not computable. A brute-force program that outputs the shortest proof of an input sentence is easy to write, but it will necessarily run forever on certain inputs; there's no computable way to know when to stop searching."

"The Kolmogorov complexity is an uncomputable size. So we won't be able to find the lowest complexity in general, no matter how powerful our theory is."

What does this mean to you in basic terms? And, can this be circumvented? Is there really no other way to compute or ascertain a theorems complexity in mathematical logic?