upvote
I haven’t been following the AI proof stuff very closely, but the impression I got was that these models are producing massive Lean programs that prove the statement one way or another, but are quite difficult to fully understand.

Actually, I have to admit I don’t really know what math is. With physics we suspect there’s a universe, and when we study physics we’re improving our description of the behavior of that universe, right? The universe exists whether or not we know how it works.

Eventually, as you suggest, maybe we’ll hit math that won’t fit in anybody’s head at all. What is the nature of mathematics that doesn’t fit in any human’s head? Does it even exist in some sense?

reply
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.

reply
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.

reply
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.
reply
What you are saying implies that by some technique that hasn't been discovered yet, we can make the models to have the capabilities of extrapolate the information they are trained on and also interpret that what they are extrapolating are Riemann-capable hypothesis. I do believe it will accelerate the discovery of that "vast universe of mathematical depth that's beyond our ability" but at the cost of removing the "fun part" of solving the problems. Not sure if the community is willing to do that.
reply