Comment by xiaoyu2006

It's completely different things. Math itself is abstraction. Lean is formalized abstraction that don't let you write "it is immediately obvious that"