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
8
votes
2
answers
358
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 + ...
- 99k
9
votes
2
answers
492
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'...
- 77.5k
10
votes
2
answers
680
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 ...
- 77.5k
9
votes
3
answers
455
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....
- 99k
11
votes
0
answers
695
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 ...
- 1,188
20
votes
2
answers
829
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). ...
- 77.5k
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 ...
- 99k