50
votes
Accepted
What are the main differences between Coq and Lean?
As to theoretical differences, the most thorough presentation I know of is found in section 2.8 of Mario Carneiro's master thesis, which I will try to summarize here:
Coq has universe cumulativity, ...
- 1,682
37
votes
What are the main differences between Coq and Lean?
It it hard to write an answer here which is not just a technical list of differences in specification, but also avoids the flame war of "my theorem prover is better than yours". (I'd be ...
- 9,195
36
votes
What will happen to mathlib when we transition to Lean 4?
BIG UPDATE
The port to Lean4 is officially complete. There is a couple changes that we are still hoping to officially put into mathlib3 before moving it into ...
- 1,445
34
votes
Accepted
What is the difference between `leanprover` and `leanprover-community` GitHub repositories?
https://github.com/leanprover is the official Lean organization, and contains the original works being built by Leo de Moura and his team. It also is in particular where development of Lean 4 is ...
- 576
31
votes
Accepted
In Lean, what do double curly brackets mean?
Single braces{⋯} indicate a maximally inserted implicit argument and {{⋯}} a weakly inserted implicit argument, as explained in ...
- 9,812
21
votes
Accepted
Lean "nonempty" vs "inhabited"
The difference between Nonempty and Inhabited is that Nonempty A : Prop but ...
- 1,599
20
votes
What exactly is setoid hell?
Setoid hell means that you are doing by hand the work of a compiler.
A setoid is just a type equipped with an equivalence relation. One can then define functions between setoids as functions between ...
- 2,333
18
votes
Accepted
Tutorials for formalizing mathematical definitions/statements in Lean
Lean for the Curious Mathematician 2020
You seem to be the exact right audience for this workshop. We have video recordings on youtube: https://www.youtube.com/watch?v=8mVOIGW5US4&list=PLlF-...
- 786
18
votes
Accepted
What is the difference between refl and rfl in Lean 3?
So you are correct that refl is a tactic, and rfl is a term, so for example:
...
- 1,445
17
votes
How to track backwards-incompatible changes in mathlib?
The mathlib commit log serves as a de facto changelog. Since the project updates far too frequently to keep a traditional changelog, a good method if you know approximately when breaking changes ...
- 593
17
votes
Accepted
How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?
To address a most important point, as suggested by Andrej Bauer, Lean's intended model is one where types are sets. Mario Carneiro showed in his master's thesis that Lean has such a set-theoretic ...
- 9,195
16
votes
Accepted
Finding symbols in Lean
Unicode character input is an editor feature, so this answer is specific to VSCode.
If you have a Lean file open in VSCode, you can hover over a unicode symbol to see what input commands are available....
- 593
16
votes
Is there software for interfacing Lean code with LaTeX?
The tool Alectryon https://github.com/cpitclaudel/alectryon aims to enable writing literate formal proofs, and produces very nice outputs.
E.g. https://alectryon-paper.github.io/bench/books/...
- 625
16
votes
How to search for an existing theorem in Lean?
I use three strategies to find existing lemmas: the exact? tactic, the gptf tactic and guessing the name based on mathlib naming ...
16
votes
Accepted
What does the "motive is not type correct" error mean in Lean?
This tends to show up when trying to rewrite a term that appears as a dependent argument.
To understand this, let’s see how rw actually works, by way of a small ...
- 1,904
15
votes
Accepted
In Lean, why is the exact tactic necessary when the goal is the same as a hypothesis?
My take on that is that, in their first approximation, tactics are just ways to build terms (typically proof terms), so it is expected to have basic tactics that closely correspond to the various term ...
- 1,904
15
votes
High-performance proof assistants
We have to distinguish two kinds of concurrency here:
Concurrency when checking a single proof object, implemented within the proof assistant, as supported by e.g. Coq and Lean.
Concurrency while ...
- 251
14
votes
Accepted
Proof review: Sum of nCk over antidiagonal = Fibonacci
I'll first go through piece-by-piece and suggest some local improvements.
For the induction principle, when you find yourself doing intros as the first step of a ...
- 506
14
votes
What exactly is setoid hell?
Disclaimer: I know very little about Lean, so I would be happy to be proved wrong.
There is no escape from setoid hell. Lean simply gives a different way of doing the same thing one does in Coq.
In ...
- 2,300
13
votes
Accepted
Extends vs including a typeclass argument
Section 2.2 of Anne Baanen's recent paper Use and abuse of instance parameters in the Lean mathematical library gives a very nice explanation of this, referring to them as "unbundled subclasses&...
- 593
13
votes
Accepted
What is in an olean file?
(My answer is for Lean 3. I don't know how .oleans changed in Lean 4.)
Also, see this discussion on the Lean Zulip.
TL;DR
An ...
- 9,195
13
votes
Accepted
What are the differences between theorem, example, def, etc?
An outline of the differences in Lean 4, which you mentioned is the version you are interested in:
A def is the primary way to define a named function / value in ...
- 351
12
votes
Accepted
Does Lean have a standard ASCII representation?
There is no standard ASCII representation that is equivalent to an arbitrary Lean 4 file using Unicode, and I'm not aware of such a thing for any other language. (Isabelle uses that encoding because ...
- 1,682
12
votes
How usable is Lean for constructive mathematics?
First, a quick disclaimer: I am not a constructivist! However, I am a logician and I care about aspects of constructive mathematics and I really care about computability in general.
As Jason mentioned,...
11
votes
Accepted
Representing $\Bbb RP^2$ in Lean: building a type representing a particular set
Let me answer your immediate question first with the following code snippet (which relies on mathlib):
...
- 166
11
votes
Is there software for interfacing Lean code with LaTeX?
There is also Patrick Massot's https://github.com/PatrickMassot/leanblueprint which is powering
https://leanprover-community.github.io/sphere-eversion/blueprint/
https://leanprover-community.github....
- 786
11
votes
How hard is computing integrals in Lean?
I'm going to inflate Mario's comment to an answer: You can absolutely write tactics in Lean to do this. What you'll be doing is creating a large part of a CAS, but as a Tactic. This would be largely a ...
- 429
11
votes
Strong induction on ℕ with function α → ℕ
Here's how to prove Andrej Bauer's corrected statement using the induction tactic:
...
Eric♦
- 971
11
votes
How usable is Lean for constructive mathematics?
I think given the other two positive answers, I want to temper expectations.
Lean 4 is designed for classical mathematics in mind, and the developers don't have any current plans to support ...
- 9,195
11
votes
Accepted
In Lean, contradiction tactic failed but actually goal accomplished
The issue is the ; at the end of the long line. This is causing the {right, ...} block to be applied to all goals, meaning that ...
- 1,599
Only top scored, non community-wiki answers of a minimum length are eligible