If the proof is hundreds or thousands of lines of Lean, it’s not clear that the AI will be able to provide an insightful “why”, instead of just dozens of microsteps.

And if it can provide insightful “whys”, that still correlates with beauty then.

Given the slop-like nature of what current generative AI tends to produce, I wouldn’t however count on the latter quite yet.