In accordance with our meta agreement, since one candidate received more votes than the others, we have a new featured language! Throughout October 2021, our Language of the Month will be:
What's a Language of the Month?
See the meta post for nominations. In short, during October, those who wish to participate should learn Lean, and use it to solve challenges.
Information about Lean
Taken from the nomination post
- Can be used as a programming language with formal verification support. The upcoming stable release (Lean 4) will make it even easier to program in Lean.
- Strong focus on approachability and soundness.
- There is an active community of Lean users ready to answer your Lean questions.
- Intimidating documentation. It's much faster to ask a question in the Zulip chat than trying to parse the (often very complex and dense) mathlib docs and Lean reference.
- You can't really Google anything about Lean. Lean is relatively obscure. But hey, the same goes for other theorem proving languages, right?