Sure, but who will care?

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.