Let's see how long (if it ever happens) it takes for models to generate motivated explanations (possibly done via the Manim library or something like it) along with their Lean proofs. Grant Sanderson is right that this is kind of subjective but so is Art and I'm very enthusiastic about AI generated Art.