Also interesting as a programming language:
Is the experience here much different from Idris? The latter was more a language that can also be used for proofs, whereas Lean came out of a proof assistant. Does that lead to much difference in use, or do the approaches essentially converge?
Looking briefly at the example code, it seems pretty similar.
I think they end up similar. Although Lean 3 is much more geared towards writing proofs with the addition of mathlib [0] which aims to be a library of formalized mathematics.