Much (most?) of math consists in transmission of it (according to Thurston [1]), a 1000-page proof with no possibility of transmission is mostly useless. The proof of Fermat's last Theorem is important in itself, and adds much more than the mere result.
I am not talking about the supposed "beauty" of a proof (I do not believe in that concept, rather in "elegance", which is not the same), I am talking about the proof itself, and the insights it provides.
An inscrutable 1000-page Lean proof may have low transmissibility amongst humans, yet extremely high transmissibility amongst AI mathematicians.
Probably AI mathematics needs a specially constructed or trained translation or compression system (likely also an AI system) that helps transmit dense Lean proofs back into human-style thinking. We may even see an entire field develop around creating human-comprehensible compressions of vast formal breakthroughs in mathematics. Such an activity would almost certainly be both art and science -- there's some objectivity in that certain abstractions or definitions inherently cover more ground more efficiently, yet there's also a deep creativity and artistry in finding compressions that are adapted to the specific 3+1D spatiotemporal intuition of the human mind. Perhaps with time this will keep a lot of the originality and creativity of research mathematics alive -- maybe with that work having even more centrality than it does today.
Instead of seeing this all as a loss of beauty in mathematics, I choose to see it as the beginning of a new age, which will bring entirely new problems to solve, yet also accelerate discovery at an exponential rate.
Mathematics is a language for humans, not just for machines. We may agree to let machines "do their thing" for as long as they want but to what purpose? Just creating "results"? What is a mathematical result by itself?
Unless, of course, we are willing to give machines the responsibility of building bridges. Subject on which I do not have a clear opinion yet.
But just hard drives (or whatever) filled with bytes representing strings representing nothing any human will ever understand... I am not for it (as of now). There are much more important problems to solve.
I'm not sure why we would assume that AI-generated or AI-assisted mathematics would never amount to anything useful in the real world. I would expect the opposite: the usefulness and explanatory power of mathematics has been riding an exponential over the last several centuries.
Maybe I didn't do a good job explaining it, but the rest of my prior comment was about connecting AI-generated results back into human-style thinking. Inevitably, in the far future, it's not unreasonable to assume the world will be dominated by synthetic robots controlled by artificial intelligence, and there will indeed be a point where AI builds not just bridges but vast planetary, interplanetary, and space-based infrastructure projects beyond the ability of our current civilization. At that point, mathematics may permanently move beyond the grasp of the human species. You can't teach a dog general relativity. Surely, there are truths in mathematics (and possibly physics) you cannot teach a human. Not to digress, but for me, this kind of threshold is what a term like "superintelligence" means -- the point where an intelligence is discovering truths that cannot be taught back to humans because we're not smart enough. So far, our contact with this kind of intelligence has been limited to one-off, highly specialized cases (like chess) that have little grand implication for civilization, but that won't always be the case.
But, for today and probably at least our lifetime, to make them useful major AI advances in math will need to be "compressed" back into the specific network and "towers" of concepts and abstractions that human minds specifically can understand and intuit about. So I think both directions of formalization are equally important: translating natural language statements (theorems, lemmas, etc.) faithfully into Lean and letting a theorem prover run and decoding a dense Lean proof back into natural language (which, in some ways, is the more creative and open-ended problem -- there is no one right answer).
"Beauty" is something I cannot define. "Elegance", as I use it, is the use of tools as precisely as possible. It is a technical term, whereas "beauty" I cannot define.
When writing code I also believed in the "beauty" and "elegance" because IMO it opens up all kinds of different opportunities that involve using or organically growing or improving that code. It turns out that if it doesn't solve a quantifiable problem, (mostly) nobody cares. And the pace of innovating in the field outgrows the pace (by a large) of keeping things "beautiful and elegant".
> a 1000-page proof with no possibility of transmission
Have you actually looked at LEAN proofs? They are typically split into small bite size definitions and proofs, making it easy to dive in where you want, and skip what you don't care about, while knowing that you can trust the conclusions.
I personally think that having hundreds of mathematicians working together as a team is a beautiful thing.
I am not talking about the supposed "beauty" of a proof (I do not believe in that concept, rather in "elegance", which is not the same), I am talking about the proof itself, and the insights it provides.
[1] https://www.ams.org/journals/bull/1994-30-02/S0273-0979-1994...