Language of the Month for October 2021: Lean

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:

Lean

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.

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.

Pros

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

Caveats

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

List of all Lean solutions posted in October 2021

(First time posters highlighted in bold)

• add entries in the form:

[<challenge title>](https://codegolf.stackexchange.com/a/<answer-ID>) by [username](https://codegolf.stackexchange.com/users/<user-ID>)


List of all Lean tips posted in October 2021

• add entries in the form:

[<tip title>](https://codegolf.stackexchange.com/a/<answer-ID>) by [username](https://codegolf.stackexchange.com/users/<user-ID>)


List of Lean-related challenges posted in October 2021

• add entries in the form:

[<challenge title>](https://codegolf.stackexchange.com/q/<question-ID>) by [username](https://codegolf.stackexchange.com/users/<user-ID>)