Questions tagged [lean3]
Lean 3 is the previous version of the Lean theorem prover, and has an active "community" release. If using the final "official" release from 2019 (3.4.2) which is incompatible with [mathlib], make this clear in your question.
34
questions
1
vote
1
answer
291
views
How to write this non-constructive proof in Lean?
There is a theorem which says that there exists two irrationals $x, y$ such that $x^y$ is rational.
An interesting proof in classical logic is the following:
Consider $u = \sqrt{2}^{\sqrt{2}}$.
If $u$...
- 273
2
votes
1
answer
96
views
Lean: what does the syntax `variable [ring R]` mean?
I have written a simple Lean program, inspired by things I found here and there, which compiles as shown in the web editor:
...
- 273
2
votes
0
answers
28
views
Proving (((finset.range 50).erase 0).erase 1).sum id = (finset.range 50).sum id - 1
I'm trying to prove the statement (((finset.range 50).erase 0).erase 1).sum id = (finset.range 50).sum id - 1 in Lean 3. The mathlib theorem ...
- 21
1
vote
2
answers
179
views
How to parse Lean 3(?) theorem statements to JSON AST
I'd like to take a .lean file, and extract from it all the theorem statements into a fully-elaborated unambiguous textual format that is morally isomorphic to the ...
- 1,062
0
votes
0
answers
166
views
Porting Lean 3 to Lean 4 Process (and the state of general integration in Lean 4)
I found this reference for measure-theoretic integration in Lean. However, I cannot find any integration in the Lean 4 Measure Theory library. Have these not yet been ported, or can they be found ...
- 446
0
votes
2
answers
106
views
Differential Topology and Differential Geometry Porting to Mathlib4
Simple question, but I started working with Lean after Lean 4 came out, so I'm not familiar with Lean 3. To what extent have the Mathlib3 differential topology and differential geometry libraries been ...
- 446
2
votes
1
answer
89
views
Recursive definition of a sum of squares
I am trying to formalise in Lean3 the notion of sum of squares in a ring.
If $ A $ is a ring, $ n $ is an integer and $ f $ is a function from $$ F_n:= \{ i \in \...
- 145
2
votes
1
answer
130
views
Vectors in Lean
In Lean vectors are implemented using
def Vec (a : Type u) (n : Nat) :=
{ l : List a // l.length = n}
I think there is another way to do this without lists:
<...
- 446
5
votes
2
answers
302
views
Type Theory Lean 3 to Lean 4
I'm aware of Lean's type theory. Did the type theory of lean change at all as we moved to Lean 4? Are there any references to this?
- 446
2
votes
1
answer
132
views
Equality of two functions
I am wondering about definition of functions in Lean and proving equality (in some sense to be defined) of two functions.
Note: I have consulted the answer to the following related question but it ...
- 145
1
vote
2
answers
916
views
Make ChatGPT write formal proof from natural language proof
I know very little about proof assistants, but I played a little with Lean, so I have some basic knowledge of how they work.
I was curious whether I could make ChatGPT convert some natural language ...
- 121
0
votes
1
answer
109
views
A chain of coercion in Lean fails to infer the correct type automatically but each separate step does
Context
I have defined two structures corresponding to a group and a subgroup :
...
- 11
2
votes
3
answers
408
views
How can I use a dummy variable to prove a lemma in Lean3?
I have the following definition for the operator D:
noncomputable def D: (ℝ → ℝ) → (ℝ → ℝ) := λ f, deriv f
I want to prove that ...
- 21
3
votes
1
answer
70
views
Are there squeeze-versions of ring and abel?
In Lean, it is recommended to use squeeze_simp to generate simp only [a bunch of lemmas] for two reasons:
(1) Otherwise the ...
- 183
2
votes
1
answer
204
views
Eliminating "Exists Unique" in Lean 3
In Lean 3, similar to this question, I want to exhibit a witness of $x$ of $P(x)$, given that $\exists x,P(x)$. The difference is that I can also prove $\exists! x,P(x)$, so there is exactly 1 element ...
- 23
0
votes
1
answer
419
views
Installing relevant packages for Lean's math lib
I'm using the Lean computer proof assistant on my Mac.
I tried to import data.nat.basic from lean's documentation, just like this:
import data.nat.basic
I get this:...
- 381
2
votes
1
answer
94
views
Why does an internal term produced by Lean's equation compiler have holes in it?
Section 4.7 of the Lean reference manual (version 3.3) gives an example of a division function defined by well-founded recursion. I used the #print command to ...
- 35
1
vote
1
answer
74
views
Code obtained from printing a definition from the Lean 3.46 equation compiler does not type check. Why doesn't it, and how can I fix it?
In the example below, the fibonacci function is defined via the Lean equation compiler. However, there seems to be a problem with the code that is obtained from running ...
- 35
0
votes
1
answer
97
views
Prove in Lean that ∀ i, 0 ≤ X i → ∃ i, X i > 1 → ∑ i, X i > 1
How to prove that if a term in a sum is > 1 then the sum is > 1?
...
- 163
7
votes
1
answer
272
views
Cardinality of Type in a given universe
I'm trying to determine the cardinality of Type u in Lean 3. So far I've been able to prove two inequalities:
...
- 173
2
votes
0
answers
192
views
Proof of a certain proposition not using classical logic
I'm self-studying the textbook Theorem Proving in Lean, and there's one exercise from Section 3.7 that I'm stuck on. The exercise asks for a proof of the proposition ¬(p ↔ ¬p) that does not use ...
- 121
5
votes
1
answer
212
views
Define a new Type in Lean: Tensor power of vector space
I want to define the tensor power of a vector space from the Lean library mathlib.
Here's the draft I have so far:
...
- 163
7
votes
1
answer
945
views
In Lean, contradiction tactic failed but actually goal accomplished
I've been playing with Lean, trying to prove the next lemma:
lemma l1_cl (A B C : Prop) : ((A → B) → C) → ((A ∧ ¬ B) ∨ C) :=
...
- 195
6
votes
2
answers
230
views
How to prove in Lean that sums are distributive?
Assume we are given three types in Lean.
constants A B C : Type
There is a canonical map of the following form.
...
- 722
2
votes
1
answer
202
views
Lemma about splitting of homogeneous polynomial equations into irreducible equations
Proof assistants, and Lean, are completely new to me.
How can I derive the following simple lemma in Lean?
How can I let Lean check if the lemma is correctly written?
How can I let Lean check if the ...
- 131
13
votes
1
answer
615
views
Lean "nonempty" vs "inhabited"
In the init/logic.lean file of the Lean 3 standard library, nonempty and inhabited are defined. It seems like these two classes ...
- 686
9
votes
1
answer
591
views
How to define curry in Lean
I just started with Lean and with this nice SE.
In the official web book/tutorial, when explaining definitions https://leanprover.github.io/theorem_proving_in_lean/index.html they ask to complete this ...
- 193
13
votes
0
answers
413
views
How to speed up Lean?
I've recently been writing my first somewhat serious proof in Lean. While doing that, I noticed that Lean gets slower very fast with increasing length of the proof (slower in the sense that whenever I ...
- 471
16
votes
1
answer
699
views
What does the "motive is not type correct" error mean in Lean?
Sometimes, trying to use rw in Lean, we get an error saying
motive is not type correct
What does this mean? Often ...
- 898
8
votes
2
answers
384
views
Strong induction on ℕ with function α → ℕ
I have the following problem. I have a type $\alpha$, function $f : \alpha \to \mathbb{N}$ and predicate $P : \alpha \to \mathrm{Prop}$ and I want to prove that for all $a : \alpha, P a$.
How could ...
- 137
11
votes
1
answer
217
views
Explicit vs implicit universes in lean
I've seen in mathlib several cases where the universes are explicit, that is Type u instead of Type*. Is there any advantage in ...
- 213
19
votes
2
answers
489
views
What is the difference between refl and rfl in Lean 3?
I already know that refl is called a tactic, and that rfl is a term; can you explain with examples how they technically differ? ...
- 400
16
votes
1
answer
163
views
Extends vs including a typeclass argument
In the Lean mathlib, I see some places where a typeclass argument is included in a class definition, such as locally_finite_order. In other places, I see the "<...
- 686
30
votes
1
answer
549
views
In Lean, what do double curly brackets mean?
In Lean, explicit function arguments are enclosed in round brackets and implicit ones in curly brackets, as in this example:
...
- 997