How is this relevant here? AI helps you understand the why -- it literally discovers the proof and hands it to you with explanations. It hands you the proof that you would have otherwise not found easily.

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.

I don't know how you think it only gives you Lean - it gives you everything including the explanation. You can actually ask it explanation using you know.. natural language.

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

Yeah it can, you just have to ask it. It has a good interface for it - text! I think you misunderstand how this tech works, its not just spitting out things. It has the understanding also and you can verify it by asking!