# 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
Filter by
Sorted by
Tagged with
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 ...
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: ...
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 ...
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 ...
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

• 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? ...
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'...
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. ...
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 "<...
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 ...
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: ...
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