Why do you believe that learning Lean is a better use of time when the AI is clearly better at writing and interpreting Lean than it is writing quality papers? At this point, Lean is for autoformalization, no one is really supposed to read it.
Well, you don't necessarily need to read the proof, but the proof is useless if you don't read the specification.
Well, you don't necessarily need to read the proof, but the proof is useless if you don't read the specification.