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.
91
questions
3
votes
2
answers
158
views
Like arbitrary, but for nonempty instead of inhabited
I wrote some code that used a [inhabited ι] assumption, and then used arbitrary ι in the proof. The mathlib linter then ...
- 1,614
22
votes
4
answers
1k
views
How usable is Lean for constructive mathematics?
In my answer explaining the differences between Lean and Coq, I emphasized that Lean is "essentially classical" mostly due to sociological norms. Nonetheless, even after posting that, I ...
- 5,748
13
votes
0
answers
322
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 ...
- 451
16
votes
1
answer
550
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 ...
- 733
8
votes
2
answers
311
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
12
votes
2
answers
240
views
Does Lean have a standard ASCII representation?
From Lean 4 tutorial, I learned that
In the Lean standard library, you often see Greek letters to denote
types, and the Unicode symbol → as a more compact version of ->
and you can also type the ...
- 1,516
35
votes
3
answers
1k
views
What exactly is setoid hell?
One of the only arguments I've heard about why Lean is better than Coq is that you can construct quotients of built-in structures by default. (In Coq, you apparently have to use Setoids instead of ...
- 451
7
votes
1
answer
135
views
How does Lean choose which decidability instance to use?
Suppose two separate files define decidability instances for a particular predicate in different ways. If I import both of these files, and attempt to run ...
- 666
11
votes
1
answer
190
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
5
votes
0
answers
169
views
What would a fully classical and fully univalent ITP and library look like?
Consider two developments in dependent type theory:
Lean’s mathlib library (as well many other ITP libraries) is unashamedly fully classical. There is no ...
- 5,748
8
votes
1
answer
141
views
How to quickly look up what constructor/lemma I should use in Lean4?
When writing this answer, I had a hard time finding the lemma I needed to prove 2 ≤ 3. In Agda, when I have a goal, I can press ...
- 5,424
6
votes
1
answer
76
views
Lean: how to use the refine_struct tactic for commutative ring structures?
Suppose I want to make bool (i.e. the type {ff,tt} of boolean values) into a commutative ring. The following works:
...
- 977
6
votes
1
answer
199
views
How to install Lean-4 stable only?
I followed Lean documentation to install Lean 4 on my Ubuntu Linux (20.04 LTS) using the elan option described there, and updated it to Lean4 ...
- 1,516
12
votes
1
answer
141
views
Lean: problems with visually indistinguishable instances
I will describe a problem which I have in fact solved, but with considerable pain. My question is whether there are better methods for dealing with similar issues.
Lean was giving me messages that ...
- 977
6
votes
2
answers
162
views
How do we resolve metavariables that appear in hypotheses and targets in Lean?
There are two related questions that I expound on below. It might seem like these aren't quite related, but they are both about how to deal with meta-variables that appear when working through a ...
- 363
5
votes
1
answer
71
views
Referencing previous fields when constructing new structure
Let's say I have a simple structure
structure foo : Type :=
(a : ℕ)
(b : list (fin a))
when defining the field b I can ...
- 137
19
votes
1
answer
343
views
How hard is computing integrals in Lean?
Are there tools in mathlib which let you give computations of integrals which would roughly follow standard methods for solving them? For now let me restrict attention to some undergrad-level ...
- 988
10
votes
2
answers
111
views
Can Lean simp arguments be ordered?
I want to simplify the expression 0 * 1 * 1 * 1 * 0 using simp only [mul_zero, zero_mul]. I would like ...
- 666
14
votes
1
answer
167
views
Proof review: Sum of nCk over antidiagonal = Fibonacci
Theorem to prove:
The sum of the binomial coefficients over an antidiagonal is a Fibonacci number. More specifically, the $n$th antidiagonal sums to the $n+1$th Fibonacci number, where the ...
- 674
10
votes
1
answer
91
views
Rewriting with context in nested expressions (congruence rules)
I am trying to prove the following example in Lean 4:
...
- 275
7
votes
3
answers
186
views
Preserve equality with match expression
How can I prove that the matched pattern is equal to the original argument?
For example, in the following function, what can I write instead of sorry to prove the ...
- 275
8
votes
0
answers
115
views
Has there been any work on automated translation of tactic proofs to everyday language?
There are times when I've completed a proof with a lot of backwards reasoning, and I've kind of lost the thread of what I've actually done. It would be nice if there was something that could ...
- 363
6
votes
2
answers
168
views
How to define a recursive sequence in Lean?
Given a recursive sequence of the form
$$
f_n = \begin{cases}
c_n & n ≤ N\\
F(f_1, f_2, …, f_{n - 1}) & n > N
\end{cases}
$$
where $c_n$ are constants and $F$ is an arbitrary expression of $...
- 163
11
votes
1
answer
143
views
Representing $\Bbb RP^2$ in Lean: building a type representing a particular set
I need to work with the set of all lines in the Cartesian plane. For my context, the natural way to think of this is that a line can be described by an equation $Ax + By + C = 0$, where $A$ and $B$ ...
- 305
18
votes
2
answers
284
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
19
votes
1
answer
323
views
How to search for an existing theorem in Lean?
When proving things in a theorem prover, I am often using sizable libraries that I don’t know by heart, so it is crucial to be effective in discovering existing theorems.
What are the best approaches ...
- 1,614
21
votes
1
answer
235
views
Tutorials for formalizing mathematical definitions/statements in Lean
tl;dr: Are there any good introductions/tutorials on how to formalize definitions and theorem statements in Lean? (in contrast to introductions on formalizing proofs)
Some background: I am a phd ...
- 451
14
votes
2
answers
250
views
What is in an olean file?
It seems Lean can produce .olean files from Lean files, and the mathlib project provides an infrastructure to download olean files, which seems to allow the ...
- 1,614
12
votes
1
answer
277
views
In Lean, why is the exact tactic necessary when the goal is the same as a hypothesis?
In Lean, when proving basic theorems, one runs into the following kind of thing:
...
- 363
29
votes
1
answer
640
views
What will happen to mathlib when we transition to Lean 4?
Today, there's an exciting large-scale effort to digitize mathematics in Lean's mathematics library mathlib.
I understand that a transition to Lean 4 is looming. I'...
- 931
17
votes
0
answers
149
views
Programming language metatheory in Lean 4?
I'm looking for developments of programming language metatheory done in Lean 4. We have a calculus with a lot of mutually recursive judgements and we want to formalise its denotational semantics.
...
- 1,853
10
votes
1
answer
104
views
Is there an official recommendation for editors to input Lean unicode characters?
As mentioned in another question, the way that VSCode and other editors implement unicode characters that cannot be typed directly from most keyboards is an editor feature.
As such, different editors ...
13
votes
2
answers
178
views
Finding symbols in Lean
There was already a question here of this type but I would like to ask more generally:
If I see some strange unicode symbols being used in Lean, is there a recommended way to find out how to type them,...
16
votes
2
answers
211
views
Why does apply_instance fail to generate decidable_pred here?
Here is a stripped down version of something that is causing me trouble.
...
- 977
15
votes
1
answer
122
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 "<...
- 666
46
votes
2
answers
3k
views
What are the main differences between Coq and Lean?
Coq and Lean are two of the most common proof assistants out there (but the question of course applies to other proof assistants too).
What are the main differences between Coq and Lean? Ideally it ...
- 733
22
votes
1
answer
161
views
How to track backwards-incompatible changes in mathlib?
I am trying to update a large body of Lean code to work with the current version of mathlib. This is difficult because there have been a large number of backwards-incompatible changes even since I ...
- 977
29
votes
1
answer
417
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:
...
- 977
25
votes
2
answers
430
views
Is there software for interfacing Lean code with LaTeX?
The Natural Number Game suggests the possibility of rewriting mathematics textbooks with embedded interactive Lean code. I'm envisioning something like Google Colab or Mathematica, where you can ...
- 351
21
votes
1
answer
339
views
What is the difference between `leanprover` and `leanprover-community` GitHub repositories?
I keep bumping into references to "Lean", but then find there are two GitHub repositories for Lean:
https://github.com/leanprover
and
https://github.com/leanprover-community
Can someone ...
- 2,796
25
votes
2
answers
376
views
High-performance proof assistants
I mainly work in the field of high-performance computing (HPC). For a 2020 paper I did a Monte Carlo calculation using 24800 CPUs, and one part of the paper was about showing that even up to 24800 ...
- 1,105