I've worked for a good numbers of years in the US software industry as a compiler engineer, and am a Mathematics masters student now. I've played with proof assistants extensively, and in particular I'm currently working on a paper to formalize semi-cubical sets in Coq. Working with Coq has been most painful, and it requires spoon-feeding for verifying even the simplest results. Worst of all, it's riddled with bugs, and I'm constantly astounded at how stupid it is.
That said, Lean is a much newer proof assistant, and while it offers some nice conveniences, it will take at least a decade before its power is comparable to Coq.
Mathematics is a solitary activity for good reason. Much of the work happens on pen-and-paper, and it takes months of toil to prove a result. No serious mathematician is going to go through the pain of encoding her proof in a proof assistant, and spoon-feeding it to verify every little result.
What's the news? That several computer scientists in the area are doing the work of formalizing simple mathematical results in Lean. Don't mistake Lean for some ground-breaking new technology; sure, it has a thriving community, and offers many conveniences, but the level of abstraction it offers isn't even close to the level of abstraction that my subject offers (I study stable ∞-categories).
Sure, if you want to do the thankless work of formalizing well-known results from group theory, ring theory, or vector spaces in Lean, be my guest. But don't be under the illusion that it's going to change the way mathematics is fundamentally done. The work is comparable to type-setting a document, except that it's a LOT more painful.