2022 Developer Survey is open! Take survey.

Questions tagged [lean]

Lean is a proof assistant from Microsoft Research, and its associated language. Note that challenges that require the answers to be in a specific language are generally discouraged.

Filter by
Sorted by
Tagged with
8 votes
2 answers
327 views

Every Pong is Abelian

Part of the lean Language of the Month A pong* is a set \$P\$ with an operation \$+\$, that satisfies the following properties: \$ \forall a, b \in P : (b + b) + a = a\\ \forall a, b \in P : a + (b + ...
user avatar
  • 84.9k
9 votes
2 answers
484 views

Lean golf: List Game Lv2 (is_in_append, is_in_rev)

The title is an homage of the Natural Number Game, which is a nice interactive tutorial into proving certain properties of natural numbers in Lean. The definitions used in Lv1 will be reused here. I'...
user avatar
  • 62.1k
11 votes
2 answers
664 views

Lean golf: List Game Lv1 (rev_rev)

The title is an homage of the Natural Number Game, which is a nice interactive tutorial into proving certain properties of natural numbers in Lean. Given that the previous two were slightly too ...
user avatar
  • 62.1k
9 votes
3 answers
398 views

Tips for golfing in Lean

Lean is a theorem prover and programming language. It's also as of writing the Language of the Month! What tips do people have for golfing in Lean? As always, tips should be specific to to Lean (e.g....
user avatar
  • 84.9k
13 votes
0 answers
436 views

Lean golf: Balanced Bracket Sequence

Ungolfed, ugly, horrible proof to help you make progress on this challenge: https://gist.github.com/huynhtrankhanh/dff7036a45073735305caedc891dedf2 A bracket sequence is a string that consists of the ...
user avatar
21 votes
2 answers
680 views

Lean golf: Pascal vs. Fibonacci

The Pascal's triangle and the Fibonacci sequence have an interesting connection: Source: Math is Fun - Pascal's triangle Your job is to prove this property in Lean theorem prover (Lean 3 + mathlib). ...
user avatar
  • 62.1k
24 votes
2 answers
2k views

∀ a b. a + b = b + a

This question is a part of the lean LotM. A ring is a type of structure that takes the rules of addition and multiplication we are familiar with and abstracts them, so we can reason about them. To do ...
user avatar
  • 84.9k