Nah, if it produced the proof in Lean which is automatically verified to be correct, you could then just write a natural language version of the proof to accompany it (often using AI to do that part too). That's becoming the standard for AI math these days. Generating purely informal natural language proofs via AI is fundamentally bottlenecked by requiring rare professional mathematician review on every single candidate output proof.

What a ridiculous thing to say. If it was verified in Lean we could be much more confident the proof is correct.

Why not both? Not sure why you're presenting this as one or the other.