Language of the Month for October 2021: Lean

Question

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.

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.

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.
• There is an active community of Lean users ready to answer your Lean questions.

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?

Resources

• Chatroom
• Tips for golfing in Lean
• Try it online!
• GitHub repo (Lean 4)
• GitHub repo (Lean 3)
• GitHub repo (mathlib)
• The Natural Number Game
• Community home page
• Official home page
• Zulip chat

Answer 1

List of all Lean solutions posted in October 2021

(First time posters highlighted in bold)

• Replace twos with threes by Wheat Witch

• Is it a row of Pascal's triangle? by Wheat Witch

• What an Odd Function by Wheat Witch

• ∀ a b. a + b = b + a by Anders Kaseorg

• ∀ a b. a + b = b + a by Mario Carneiro

• Lean golf: Pascal vs. Fibonacci by Anders Kaseorg

• Lean golf: List Game (rev_rev) by Wheat Witch

• Lean golf: List Game (rev_rev) by Anders Kaseorg

• Every Pong is Abelian by user

• Swap Two Values in a List by user

• 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

• Introductions by Wheat Witch

• Use by instead of begin ... end by user

• The ; and <|> combinators by It'sNotALie.

• 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

• ∀ a b. a + b = b + a by Wheat Witch

• Lean golf: Balanced Bracket Sequence by Huỳnh Trần Khanh

• Lean golf: Pascal vs. Fibonacci by Bubbler

• Lean golf: List Game (rev_rev) by Bubbler

• Lean golf: List Game Lv2 (is_in_append, is_in_rev) by Bubbler

• Every Pong is Abelian by Wheat Witch

• add entries in the form:

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