But those proofs are showing that the fundamental axioms (which are generally simple and elegant) are still enough to build a complex result.

I think of elegance as not having to add epicycles, not that everything in the system has to be simple.

Also, without a working theory the, the space of possible solutions is near infinite. LLMs manage to pluck out the space of comprehensible English strings from n-dimensional hell. Even if this is done with a black box of billions of parameters, it’s still elegance in the sense that such a space even exists and was found