Over the past year, the Lean FRO has been making a big push towards making Lean a great general-purpose programming language that you can use to develop formally verified production-ready software. In this presentation, I will give an overview over the many recent innovations in Lean that are relevant for software developers, including improvements to the compiler, the standard library, and the verification infrastructure for monadic programs.