Skip to main content
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, ...
Sebastian Ullrich's user avatar
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 ...
Jason Rute's user avatar
  • 8,655
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 ...
It'sNotALie.'s user avatar
  • 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 ...
Julian's user avatar
  • 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 ...
Andrej Bauer's user avatar
  • 9,104
21 votes
Accepted

Lean "nonempty" vs "inhabited"

The difference between Nonempty and Inhabited is that Nonempty A : Prop but ...
Mario Carneiro's user avatar
19 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 ...
Pierre-Marie Pédrot's user avatar
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-...
jmc's user avatar
  • 766
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: ...
It'sNotALie.'s user avatar
  • 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 ...
Rob Lewis's user avatar
  • 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 ...
Jason Rute's user avatar
  • 8,655
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....
Rob Lewis's user avatar
  • 593
15 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 ...
Not An ITP Expert's user avatar
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 ...
Joachim Breitner's user avatar
15 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/...
Alex J Best's user avatar
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 ...
Clément's user avatar
  • 251
15 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 ...
Joachim Breitner's user avatar
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 ...
Kyle Miller's user avatar
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 ...
Couchy's user avatar
  • 2,221
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&...
Rob Lewis's user avatar
  • 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 ...
Jason Rute's user avatar
  • 8,655
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 ...
Sebastian Ullrich's user avatar
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,...
François G. Dorais's user avatar
12 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 ...
tydeu's user avatar
  • 341
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): ...
Adam Topaz's user avatar
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 ...
Jacques Carette's user avatar
11 votes

Strong induction on ℕ with function α → ℕ

Here's how to prove Andrej Bauer's corrected statement using the induction tactic: ...
Eric's user avatar
  • 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 ...
Jason Rute's user avatar
  • 8,655
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 ...
Mario Carneiro's user avatar
10 votes
Accepted

Why does apply_instance fail to generate decidable_pred here?

The predicate in Q is equivalent under β-reduction to the one in P Not according to Lean in this case. set.mem is a def, which ...
Sebastian Ullrich's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible