The problems mathematicians tend to be interested in are those that have a short description in a formal language yet the proof is likely not very compressible

The problems mathematicians tend to be interested in are those that have a short description in a formal language yet the proof is likely not very compressible via the language. I.e., you can easily get the index of any statement in the formal language of PA but finding the index of either the statement or its negation in an enumeration of the theorems of PA is significantly more difficult. It’s equivalent to the halting problem in a general sense because the statement and its negation may be independent of PA in which case the enumeration program never halts. What does this mean? These problems are like the Busy Beaver analogue for formal mathematical systems, which implies that if you solve one, in theory you solve entire classes of lower complexity problems simultaneously (similar to how BB(5) solves the halting problem for all programs below a certain complexity).