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

I have hear people make this comparison many times, but it just does not hold up under scrutiny.

I think the confusion stems from people being exposed to set theory, believing that formalisation is akin to writing those horrible set encodings of everything. Which I would agree would be akin to writing assembly.

But Lean, Rocq and Agda are all based in type theory. Which means it is more like the highest level programming language you can imagine! You have all the powers of abstraction, but you still have to convince the type checker – i.e. no “trust me, bro” casting, or even questionable while loops (“I promise this loop finishes at some point”).

These abstractions along with meta programming techniques (“tactics”) means that you can write readable correct proofs, but it takes effort. Math is extremely deep, and getting formalised all the way to the research frontier in a given subfield is a serious undertaking.

Assembly doesn't give you any safety or guardrails. It is basically the opposite. I think it would be a better comparison with something that is a very strictly typed and type checked language.

Once upon a time this was all there was, so it naturally was proven to work as it was easier than dealing with boards full of dip switches that predated them.

Naturally eventually we got macro Assemblers, followed by other attempts until FORTRAN came to be.