I think math is compressible structure. That's why we care about something like the Riemann hypothesis but, to use Tao's example, we really couldn't care less about computing the 10^10^10th digit of pi. The first compresses a vast amount of information about the primes, while the second decompresses information that we've already compressed (a few lines of code can define every digit of pi).

Most patterns that exist are incompressible. Math is basically a search for those compressions that do exist. An example I personally really like is the amplituhedron: a geometric structure that humans have just barely been capable of recognizing compresses information about scattering amplitudes and Feynman diagrams. That one happens to be within our reach, but it's right at the edge, and we can only imagine what glorious, wondrous compressions exist in abundance beyond the edge. Math accessible only to superintelligence would exist entirely beyond that edge, compressing patterns whose existence we cannot even detect using objects and constructions that we cannot grasp.

As an aside, I also think this is why AI is quickly becoming superhuman at math: intelligence is essentially a form of pattern compression.

I think part of mathematics is taking things that don't fit in our head and giving them human abstractions so they can.

Take infinity. Infinity can't fit in your head, hell, it can't fit anywhere, but you can abstract away the endlessness and look at infinities of different sizes, et al.

Now, is there a single formula for something actually represented in this world that would take most of a humans life just to read it, no idea.

The models produce both Lean code for formal verification and a traditional-style narrative proof. Like the general long-form output of frontier models, the math papers produced appear to be generally correct technically, but written in an ungraceful and sometimes hard-to-follow style, so they are often polished by a human mathematician as of today.