Yes I am aware of this one, it seems like a good intro.
I am just thinking more along the lines of - other than times where a computer is not available to us, why do we keep using traditional notion/pen and paper at all?
If everything is digitalized no one will have mark homework ever again.
I think an important thing for something like Lean to gain traction is the availability of learning resources (math 'textbooks') based on the technology so people actually use it for day to day mathematics instead of just formalizing what has already been proven without it.
I don't think many people are going to read Rudin (etc.) then try to rewrite the book or do the exercises in Lean by themselves or read through the mathlib files to see how everything is defined/proved in full generality.
Like a lot of people (I imagine), I'm not a professional mathematician working on advanced, complex problems but I would like to have the ability to have the computer check my solutions to exercises and maybe even aid me with hints for tackling problems if needed.
If math textbooks gave free use for people to rewrite them into computer format and post online it would make life a lot easier.