alt Hacker NewsHell no. Writing formal proofs has huge overhead. Lean is not a productivity tool; it's a reliability tool. It's like asking if airport security made boarding faster.
Mathematicians are also not upset about Lean. They're upset because they feel like they're becoming redundant. And that has everything to do with LLMs and not Lean.
They're upset because they're having to change. They aren't being made redundant, but they're being made redundant for the part of math they most enjoy and for which they've traditionally been most rewarded.