Questions tagged [lean]
Lean is a theorem prover and programming language, based on the calculus of constructions with inductive types. For version-specific questions, also add the [lean3] or [lean4] tags.
162
questions
2
votes
1
answer
96
views
Is there any way to approximate noncomputable functions in Lean4?
As you may know, there are some definitions in lean4 that can't be evaluated due to the noncomputable tag. Is there any way to approximate their value in lean4?
For ...
- 21
2
votes
1
answer
35
views
Proper LEAN_PATH environment variable value for Windows Lean Visual Studio project?
I have a Lean 4 test project in C:\Temp\MyProject I open with Visual Studio. In that directory, I have a Main.lean file. And, in ...
7
votes
3
answers
195
views
Why is $\Bbb Z = \Bbb N$ independent of Lean?
In this answer, it is noted
For a silly example, in ZFC with the usual encoding, $\mathbb{Z} \neq \mathbb{N}$, but in Lean it is well-known that this is independent. Of course in both ZFC or Lean, ...
- 173
5
votes
3
answers
888
views
Tools like leanblueprint for other proof assistants, especially Coq?
In my (relatively little) experience with Lean, one of the things I’ve appreciated most is the leanblueprint tool. For those not familiar with it, it’s a tool for planning a Lean development and ...
2
votes
1
answer
73
views
0
votes
1
answer
46
views
0
votes
0
answers
21
views
How does one install new dependencies to a Lean 4 programatically e.g., adding aesop by editing lakefile.lean in bash?
I have a github repo at (note it's not a Lean 4 project):
$HOME/learning_lean
with a Lean 4 project at:
...
- 333
11
votes
5
answers
2k
views
How do real-world proof assistants bind variables and check equality?
There are many possible ways to represent syntax with variable binding, such as named variables, De Bruijn indices, De Bruijn levels, locally nameless terms, nominal type theories, etc.
There are also ...
0
votes
2
answers
74
views
Proving `succ_mul` without using `nth_rewrite`
I'm trying level 3 in the multiplication world of the Natural Number Game.
My proof is given below, but I am not satisfied with it since it uses nth_rewrite.
This ...
- 3,073
1
vote
2
answers
90
views
How to write a proof of n + 0 = n in Lean 4 using the built in definition of addition for Nats and not the theorem for Nat.add_zero?
I want to do the proof of n + 0 = n in Lean 4 using mathlib 4, my attempt:
...
- 333
3
votes
2
answers
102
views
Offline install of Lean
I have fast internet, but my friend, who would like to install Lean on his computer, does not. What should I download to put on a USB stick for him? Any special installation instructions for such an ...
- 31
3
votes
1
answer
302
views
Why does `#check add_mul (R := ℕ)` return `add_mul : ∀ (a b c : ℕ), (a + b) * c = a * c + b *` instead of `add_mul : Prop`?
I don't understand why #check add_mul (R := ℕ) returns add_mul : ∀ (a b c : ℕ), (a + b) * c = a * c + b * c instead of ...
- 175
1
vote
1
answer
68
views
Define maximum of matrix entries in Lean4
In Lean4 I would like to define a function max that finds the largest entry of an $n\times n$ matrix with entries in a ...
- 193
1
vote
1
answer
99
views
Applying universally quantified equalities to propositions
In Lean, given an equality eq: e0 = e1, one may rewrite either e0 or e1 with the other one ...
- 411
2
votes
1
answer
421
views
How does one import Natural numbers in Lean 4 -- unknown identifier 'ℕ'?
I found the definition of Nat's but lean still complains that it doesn't exist. Why is it?
...
- 333