See also Terence Tao's blog posts detailing how he's using Lean 4:

https://terrytao.wordpress.com/tag/lean4/