The whole point of mathematics is to vastly exceed that natural ceiling by gradually building a framework for understanding. In fact it’s wrong to speak of a ceiling altogether. If there were a ceiling, we’d have hit it long ago.
AIs have already swallowed the entire history of human thought, but apparently they’re ’just getting started’. I can only assume you don’t know what mathematicians actually do.
We have naturally only explored the mathematical universe in the parts where telescoping via clever abstractions can get us. But there is much more. Being able to juggle more things in your mind at the same time can have qualitatively massive benefits.
Information theory and proof theory, algorithmic information theory etc has of course explored this.
Yes. The four-color theorem was the first proof like that. There have been more since, including Fermat's last theorem. Now AI systems are grinding out more.
Ultimately, you could give a few sentences to summarise the proof of FLT as long as one accepts various concepts and their (also deep and conceptual) proofs. In the case of the four-colour theorem this isn’t true because rather than being amenable to summary in words and fancy concepts it’s just a loooooad of cases to be tediously checked.
I can imagine that AI might be able to produce reams and reams of extremely tedious ‘proofs by a million special cases’ that we’d never be able (or even have thought) to do by hand, but that’s not to say there doesn’t exist an alternate, more conceptual explanation that is compressed.
In fact one might argue that facts that are ‘inherently incompressible’ are by definition uninteresting. The profound statements in mathematics are those that appear to be incompressible, yet turn out to be provable in an elegant way by a change in perspective. In this sense, noting the use of the word ‘appear’, it becomes clear that what is and isn’t interesting (and therefore what is and isn’t to be considered trivial) is entirely subjective and hence mathematics is an inescapably human pursuit. But we’ve known this for a long time.