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?