43
$\begingroup$

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 would be nice to know the differences for a mathematician not interested in foundations and for someone more involved in CS and type theory.

$\endgroup$
2
  • 1
    $\begingroup$ artagnon.com/articles/leancoq was written in 2019 and parts of it haven't dated well (e.g. the assertion that the mathematics in mathlib "plateaus quickly thereafter"), but the assertions about differences in the underlying logics are of course still valid. $\endgroup$ Feb 9 at 14:16
  • 1
    $\begingroup$ Here is a snarky (and bit out of date, 2018) take by Tom Hales: jiggerwit.wordpress.com/2018/04/14/… $\endgroup$
    – Jason Rute
    Feb 12 at 20:17

2 Answers 2

42
$\begingroup$

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:

  1. Coq has universe cumulativity, with some interesting consequences around unique typing.
  2. Coq's core syntax describes structural recursion via primitive fix and match constructs, where termination is ensured by additional typing rules, while Lean uses fundamental recursor functions that are inherently terminating.
  3. Lean has explicit universe polymorphism, meaning that id @id typechecks. Coq has experimental support for it though.
  4. Lean's inductive type signatures consist of parameters and indices, while Coq has a kind of "non-uniform" parameters in between. The latter can be encoded by the former.
  5. Coq supports mutual and nested inductive types and coinductive types natively. Lean 3's frontend supports mutual and nested inductives via encoding, but some definitional equalities may be lost. Lean 4 supports mutual inductives natively.
  6. Lean has definitional proof irrelevance, with major implications for decidability/completeness of definitional equality (section 3.1). Coq has an experimental universe SProp of proof irrelevant propositions.
  7. Lean has a built-in quotient type with reduction rule. I'll leave summarizing the "setoid hell" discussion to someone else...
  8. The set of axioms is quite different in both systems, but propositionally equivalent.
$\endgroup$
10
  • 5
    $\begingroup$ Hi! Do you have a link to any documentation of Lean 4's mutual inductives? My PhD student says it doesn't support it yet, and he would be over the moon to learn he is wrong. :) $\endgroup$ Feb 9 at 11:46
  • $\begingroup$ What do you mean by "concrete but possibly indeterminate"? Coq also has support for universe polymorphism these days. $\endgroup$ Feb 9 at 13:11
  • $\begingroup$ @NeelKrishnaswami mutual inductives themselves were never absent afair. What was missing until very recently is frontend support for well-founded recursion, without which you would have to use the mutual recursor directly. github.com/leanprover/lean4/blob/master/tests/lean/run/… (yes, linarith would really help here) $\endgroup$ Feb 9 at 13:36
  • 3
    $\begingroup$ Coq users that use the Equations plugin will have their definitions compiled down to eliminators for inductive types, equality and accessibility. This is very close to Lean's "fundamental recursor functions", and essentially means that one does not have to trust Coq's guard condition. $\endgroup$
    – palmskog
    Feb 9 at 14:31
  • 2
    $\begingroup$ @darijgrinberg What exactly are you objecting to? Both systems have LEM in their stdlib. Whether you use it is mostly a question of social norm, as described in Jason's answer. $\endgroup$ Feb 9 at 22:31
29
$\begingroup$

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 happy to delete or change this answer if it comes across too flame-war-ish or incorrect.)

Lean is essentially classical, meaning it usually uses the law of excluded middle and the axiom of choice for proofs when it is convenient. This is mostly a social norm, in that this is the standard of the Lean community and main math library, mathlib. But it is also technical in a sense in that it is difficult to avoid classical reasoning with the common tactics (and basically impossible to do homotopy type theory even within term proofs). For many just interested in formalizing pure math (except of course, say, homotopy type theory or the internal logic of some topos) this is fine and maybe preferable. If you want more flexibility on axioms or want to be able to extract algorithms from your proofs it is a problem. (However, some projects in Coq also use classical reasoning, so it isn’t like it is forbidden. It just might mean that projects which use classical reasoning won't be used by other projects which are trying to stay constructive.)

There is also a difference in community goals. I can't speak to the goals of the Coq community, but it seems to me that the main goal of the Lean3 community is to add as much mathematics as they can to the mathlib library, the main mathematical library of Lean. There is a strong emphasis on unity and cohesion in this library. It is constantly refactored to make it work well together. This (according to Lean users) makes it possible to easily combine separate areas of mathematics like rings and topological spaces (to get topological rings), but it also means that any project which is not in mathlib or trying to stay up-to-date with mathlib will quickly bit-rot. (Even Lean3 itself---at least the community edition most commonly used---changes rapidly as well, sometimes in backward incompatible ways.)

We will see in Lean4 if the focus is the same or changes. Already, many are using Lean4 as a very capable programming language, so there may be more diversity of projects and less focus on cohesion, but nonetheless, I think the contributors of mathlib would like the Lean4 version to still be highly cohesive.

There is also a lot written on the internet about say Lean vs Coq. Of course note that since Lean and (to a lesser degree) Coq are constantly changing, some of that information may be out of date. (For example, there was a time when Lean 2 supported both classical and constructive logic, even homotopy type theory.)

$\endgroup$
5
  • 1
    $\begingroup$ Isn't it literally impossible to do homotopy type theory in Lean 3-4, since the formal system enforces UIP? $\endgroup$ Feb 18 at 15:43
  • $\begingroup$ @MikeShulman I hedged. For example this suggests something (possibly quite hacky, and certainly not supported) can be done: github.com/gebner/hott3 $\endgroup$
    – Jason Rute
    Feb 18 at 16:09
  • 1
    $\begingroup$ "Lean is essentially classical" - I disagree. I've been using Lean 2/3/4 for many years, with a focus on constructive and computable mathematics. It is true that mathlib is fundamentally classical, which is why I almost never use it, but Lean itself is not. $\endgroup$ Mar 18 at 5:08
  • $\begingroup$ Well, perhaps the Lean 3 community edition is essentially classical. I wouldn't know since I had to stop using it at some point after a few things broke without mathlib. (That didn't matter to me though since I moved to Lean 4 really early and never looked back.) $\endgroup$ Mar 18 at 5:17
  • 1
    $\begingroup$ @FrançoisG.Dorais Your comment motivated me to post this question which I've been meaning to ask for a while: proofassistants.stackexchange.com/questions/1115/… $\endgroup$
    – Jason Rute
    Mar 20 at 15:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.