I'm a programmer and I'm excited to learn Lean as a new tool for thought. I find that Haskell sells itself as a programming language but the reality is quite arcane, and its tools feel slow and bloated. Lean 4 is sort of the opposite, selling itself as a math toolkit but actually having very considerately (and practically) designed support tools (VSCode integration, build system) and core language features.
I'm reading through Functional Programming in Lean now, supplementing with the Lean Manual and also Lean's prelude file, which is well commented and pretty readable. I love that the output window's contents are clickable ("failed to synthesize type class X Y Z" -> click on X, Y or Z to go to the definitions). I'm excited to try out the widget interface, which lets you complete proofs through visuospatial reasoning (see the Rubix cube project). I'm really hoping that this serves as a new tool for programming-minded people to learn math and contribute easy-to-understand proofs in a way that was never possible before. Once I've gone through the beginner materials, I want to try the math problems at the beginning of <a href="https://brickisland.net/DDGSpring2023/" rel="nofollow noreferrer">https://brickisland.net/DDGSpring2023/</a>, which has great tools for its programming projects but nothing for its proof assignments.<p>The documentation still has holes, but the Lean community is more helpful and welcoming than any other I've ever encountered, and I'm confident that I'll get an answer for every question I have.<p>For the Lean folks: an entry on learnxinyminutes is an absolute must in my book. It would be a great place to demonstrate how familiar and practical Lean can be, with its for loops and arrays and hash maps and whatever else. Generally if a language is not there, I figure it must not be mature enough to try out (Lean has been an exception for me).