Lean isn't super special in that regard. If you know Haskell or OCaml you are already pretty far along in at least being able to read Lean, as it comes out of a similar-enough tradition.
You really have to wrap your head around dependent types and _≡_. In my experience it was far more mind blowing than just FP.
But yes, you have to wrap your head around dependent types.
But that's not really what you want, right? Speaking as a programmer, I'd think you would want a language where the prerequisite is "knowing a math proof", not "some mathey PL"
> every programmer should be able to read
You want "every math major should be able to read it", not "every programmer"
Well, I was merely replying to this:
> [...] lean seems like a new foundational language family that every programmer should be able to read, [...]