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

Lean is a relatively new theorem proving language. It is very user-friendly and it has a comprehensive math library which is "slowly eating away mathematics", as Kevin Buzzard puts it.


  • 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?



1 Answer 1


List of all Lean solutions posted in October 2021

(First time posters highlighted in bold)

List of all Lean tips posted in October 2021

List of Lean-related challenges posted in October 2021


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .