Lean is also a really, really good dependently typed functional programming language. If you're on the software developer/computer science side of the coin I hi

Lean is also a really, really good dependently typed functional programming language. If you're on the software developer/computer science side of the coin I highly recommend looking into it. It's not only for maths research (although that is definitely a big focus of the majority of the Lean community). I'm working on a forthcoming series of blog posts investigating FP concepts from scratch in Lean to see how it takes with the FP-curious. The refreshing features Lean has to offer over other FP languages like Haskell is that 1. It's dependently typed which gives it a lot more flexibility to define objects that depend on types and types that depend on values, such as vectors that know their size. 2. Lean is interactive by default -- type inference is really fast, even for complex objects and functions. From my perspective Lean is a great programming language that happens to have a theorem prover available. This, in itself, can be a great feature for code that needs to provide strong guarantees about its operational parameters.