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.

Filter by
Sorted by
Tagged with
63 votes
2 answers
6k 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 ...
Ricky's user avatar
  • 958
40 votes
3 answers
2k 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 ...
setholopolus's user avatar
32 votes
1 answer
1k 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'...
Dustin G. Mixon's user avatar
30 votes
1 answer
613 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: ...
Neil Strickland's user avatar
30 votes
3 answers
1k 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 ...
Joachim Breitner's user avatar
27 votes
2 answers
915 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 ...
Jon Bannon's user avatar
26 votes
4 answers
2k 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 ...
Jason Rute's user avatar
  • 8,135
25 votes
2 answers
426 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 ...
Nike Dattani's user avatar
  • 1,165
23 votes
1 answer
342 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 ...
GraffL's user avatar
  • 471
22 votes
1 answer
419 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 ...
Guy Coder's user avatar
  • 2,836
22 votes
1 answer
175 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 ...
Neil Strickland's user avatar
22 votes
1 answer
508 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 ...
Wojowu's user avatar
  • 1,058
21 votes
3 answers
477 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. ...
Neel Krishnaswami's user avatar
19 votes
2 answers
598 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? ...
Jia Ming جيا ميڠ's user avatar
16 votes
1 answer
1k views

How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?

This document showed that Lean's impredicative universe of strict propositions breaks normalization (of proofs) in a way that canonicity and logical consistency are unaffected, because the ...
ice1000's user avatar
  • 5,974
16 votes
1 answer
814 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 ...
Ricky's user avatar
  • 958
16 votes
1 answer
194 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 "<...
Bolton Bailey's user avatar
15 votes
1 answer
734 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 ...
Bolton Bailey's user avatar
15 votes
2 answers
410 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 ...
Joachim Breitner's user avatar
15 votes
2 answers
216 views

Why does apply_instance fail to generate decidable_pred here?

Here is a stripped down version of something that is causing me trouble. ...
Neil Strickland's user avatar
14 votes
2 answers
474 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,...
Bjørn Kjos-Hanssen's user avatar
14 votes
1 answer
191 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 ...
Bubbler's user avatar
  • 674
13 votes
3 answers
775 views

Calculus of (inductive) Constructions: Do inductive definitions increase proof strength?

Question Is CiC stronger than CoC, in terms of proof strength? Context To illustrate the kind of confusion I am in, and what I'd like to learn from the answer, here is part of my inner monologue: If I ...
Max Kubierschky's user avatar
13 votes
1 answer
172 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$ ...
John's user avatar
  • 325
13 votes
0 answers
474 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 ...
GraffL's user avatar
  • 471
12 votes
2 answers
355 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 ...
tinlyx's user avatar
  • 1,906
12 votes
1 answer
533 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: ...
march's user avatar
  • 373
12 votes
1 answer
175 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 ...
Neil Strickland's user avatar
11 votes
1 answer
131 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 ...
Bjørn Kjos-Hanssen's user avatar
11 votes
1 answer
228 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 ...
mcd's user avatar
  • 213
10 votes
2 answers
130 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 ...
Bolton Bailey's user avatar
10 votes
1 answer
127 views

Rewriting with context in nested expressions (congruence rules)

I am trying to prove the following example in Lean 4: ...
Peter Zeller's user avatar
9 votes
2 answers
779 views

Learning Math Proof via Proof Assistants

I want to learn proof based mathematics and it looks like a proof assistant like Coq and Lean could be a good way to go about verifying my proofs, without needing a PhD on hand to check through all my ...
quidproquo's user avatar
9 votes
1 answer
493 views

What are the differences between theorem, example, def, etc?

What are all the differences between these keywords that allow for defining top level variables? What I have noticed so far is that theorems can't be anonymous — ...
mr snuggles's user avatar
9 votes
1 answer
612 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 ...
magma's user avatar
  • 193
9 votes
1 answer
289 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 ...
ice1000's user avatar
  • 5,974
9 votes
0 answers
129 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 ...
march's user avatar
  • 373
8 votes
2 answers
455 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 ...
burek's user avatar
  • 137
8 votes
1 answer
240 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 ...
Bolton Bailey's user avatar
8 votes
1 answer
276 views

How does Lean `simp` tactic work?

The doc at https://leanprover-community.github.io/extras/simp.html says about simp: all it does is repeatedly replace (or rewrite) subterms of the form A by B, for ...
Weier's user avatar
  • 293
8 votes
0 answers
249 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 ...
Jason Rute's user avatar
  • 8,135
7 votes
3 answers
293 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 ...
Peter Zeller's user avatar
7 votes
2 answers
728 views

Lean: dubious noncomputability

In Lean, some definitions must be marked as noncomputable, for example if they depend on the law of the excluded middle or other nonconstructive choice principles. Usually, the reason for ...
Neil Strickland's user avatar
7 votes
1 answer
962 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) := ...
Pavel Snopov's user avatar
7 votes
2 answers
225 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 $...
502E532E's user avatar
  • 173
7 votes
1 answer
329 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: ...
Matt Diamond's user avatar
7 votes
1 answer
497 views

How do I convince the Lean 4 type checker that addition is commutative?

In order to get acquainted with Lean and programming with dependent types I am trying to implement basic operations for a Vector datatype defined following the ...
BackusNaur's user avatar
7 votes
1 answer
440 views

Benefits of HoTT compared with dependent type theory like what Lean does?

I am not an expert in type theory, so I wonder what will HoTT bring to theorem proving (ITP/ATP), compared with dependent type theory? More specially, imagine Lean is implemented using HoTT, I would ...
ch271828n's user avatar
  • 171
6 votes
2 answers
332 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 ...
march's user avatar
  • 373
6 votes
2 answers
237 views

Lean and inaccessible cardinals

It seems well known that Lean's type theory is equiconsistent with ZFC + the existence of $n$ inaccessible cardinals for every $n>0$. Suppose I want to ensure that my lean proofs depend only on ZFC,...
Potato's user avatar
  • 161