Atomic vs galactic mathematics

Let's start with an informal discussion. There are infinitely many theorems. Not all of them are particularly interesting, for instance "4 is even" isn't an interesting theorem (at least to me). But let's suppose there are also infinitely many interesting theorems. The number of text strings of length at most x is finite, and hence there are finitely many interesting theorems whose proofs have length at most x. In particular, there are theorems that one cannot comprehend even 0.00000001% of its proof in a given lifetime. If the interestingness of theorems is unbounded, we can even assume that such theorems are very interesting! By the same logic, the statements of these theorems would also be arbitrarily large, hence we wouldn't even be able to apply such theorems to concrete problems ourselves. But we can draw the boundary somewhere, like "theorems that one can understand the statement during one's career". Of course, if just understanding the statement is this hard, proving it is, not necessarily but most likely, very very hard. I call this galactic mathematics, as opposed to atomic mathematics that is concerned with finer grained details (set theory, proof theory, etc…). One can only do galactic mathematics by using major results as black boxes. If galactic mathematics becomes feasible, I wonder what kind of macro-structures and applications would appear. Most mathematics until now is much closer to atomic than galactic. By analogy, if one is too concerned with trying to understand some given atoms one may fail to see the big picture about an organism or ecosystem.