Lean is particularly exciting because of the work Kevin Buzzard has been doing in the Xena project:

https://www.ma.imperial.ac.uk/~buzzard/xena/

He started by getting undergraduates to tackle formalising the maths they did in Lean, and his success with this as a didactic tool has spread the idea among quite a lot if mathematicians.

Yes, progress is under way! It's been a few years since I tried to plumb these depths, it's probably time to look again. But I don't need to look to know that we're not there, where "there" means both accessible and widely adopted.