If no one understands it, it may as well have not happened. There's not much incentive to understand or internalize the results generated by AI. A human operator gives it a prompt and it produces some lean proof no one wants to (maybe can) read.
Without the community of human mathematicians internalizing the proof, simplifying it, and re-communicating it to others we end up losing the main output of mathematics as an institution.
The questions I have are:
* is the structure of the generated proof even compressible/elegant to humans in a way that lends itself to being understood?
* is it possible to transform the proofs to ones that are elegant without redoing all the work?
* are there incentives to do any of this at scale?
You can always hypothesize that at some point in the future (maybe 5 years? maybe later?) the models will be indistinguishable from humans and there will not be any functional difference at all. It's possible, but we're not there yet. And, as they say, past performance does not guarantee future results. Many technologies plateau at some hard ceiling of performance. Moore's law has had an unusually long run, but it's not a universal rule.