> Imagine asking an AI to generate the whole numbers in order, from 0 on up. You could spend trillions of dollars having it fill up datacenter after datacenter with lists of numbers. The more we spend on the project, the more the list would start including some very big and important numbers. But what would actually be accomplished?

> Consider this and then consider how it applies to every number in any dataset and everything an AI generates: with our normal human understanding of a number, the number theoretically contains all of the meaning of that number. A number intrinsically contains the fact of whether it's prime, whether it's irrational, whether it's a counterexample to the Riemann Hypothesis, all facts known and unknown. You don't need a human to interpret the number in order for the number to mean what it means. In fact, the longer a human spends interpreting, the more meaning they might find that a number intrinsically has in and of itself. And yet... can you think of a less meaningful way to fill up a datacenter than with an ordered list of numbers?

> Listing all possible proofs out of context, whether in order or randomly, would hardly be more meaningful than listing numbers. Almost all possible proofs are trivial and meaningless, mathematicians select for the fun stuff.

> But I will say, since it seems every player in the US government and economy have committed to all jumping off a cliff together in a stubborn wish to cover the country in datacenters, I could think of worse applications than to fill them up with every possible mathematical proof below a certain size.

> You'd end up with a Library of Babel of proofs.

> You can imagine the quality of literature you'd get if you trained an LLM on the Library of Babel, which contains every possible book (or combination of characters that fit in 410 pages). The library, by itself, functionally contains no information whatsoever. The LLM trained on it would be a literal smooth-brain with no correlations to wrinkle up those gradients.

> Without the context of language and how it’s used by people, a great work of literature is just another possible random combination of letters. This can be represented as a point in multidimensional space, and a computer can guess that maybe there's more things of interest to humans near where the stuff we already like is, but only humans know how to push further into unknown directions of multidimensional space that are interesting and worthwhile.

> Whenever a company or person shares something “AI generated” that seems pretty good, that tells me that the AI must necessarily be using a lot of human-created data in that same area. The AI can not have leapt there on its own, even if it might look like it did to a person not aware of the scope of human-made work that went into it.

> The Mathlib of Babel problem is one reason why, in my view, formal math and AI are just one tool that might be useful for some math sometimes, not the end of mathematics or the future of mathematics. Formal mathematics and algorithmically-assisted proofs are not my personal aesthetic but I think it should be somebody's, and it's not like our fragmented field doesn't know how to handle another specific expertise joining the mix. We've already folded them in.

Found this interesting and thought-provoking. Why do we care about these proofs? Why do we care about this art, or this code? Because it is what is useful and interesting to humans.