As someone who is currently getting a PhD in mathematics I wish I could use Lean. The main problem for me is that the area I work in hasn't been formalized in Lean yet. I tried for like a week, but didn't get very far... I only managed to implement the definition of Poisson point process (kinda). I concluded that it wasn't worth spending my time to create this feedback loop and I'd rather work based on vibes. I am jealous of the next generation of mathematicians that are forced to write down everything using formal verification. They will be better than the current generation.
I would call this "not thinking on the margins"
Some early results: