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.

7 questions
Filter by
Sorted by
Tagged with
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 + ...
• 84.9k
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'...
• 62.1k
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 ...
• 62.1k
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....
• 84.9k
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 ...
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). ...
• 62.1k