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.
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.