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.

[1] https://www.ams.org/journals/bull/1994-30-02/S0273-0979-1994...

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.

What is the difference between "beauty" and "elegance" of a proof?

You are mixing a lot of categories here -- beauty, verbosity, utility, elegance, insights.

Why all that when you just need one thing: truth.