The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/24/2016 07:17 PM, Saulo Araujo wrote:
> Hi,
>
> I recently discovered the Lean Theorem Prover (
> https://leanprover.github.io/about/). I did some toy experiments with it
> and and, at least in this first contact, it seemed similar to Coq.

It looks eerily similar to Coq.  The syntax and semantics both seem very 
similar.  One of the minor semantic differences I saw in a quick 
walk-through is that Lean's Prop universe has built-in irrelevance, 
while Coq's Prop can get irrelevance via an additional axiom.  Even the 
tactic names are similar.

It almost looks like Lean is a project to rebuild Coq that doesn't have 
to pay homage to backward compatibility.  I'll bet there are some Coq 
developers that would be quite envious of that position. Although, it is 
written in C++ instead of OCaml, so maybe their envy would turn to 
schadenfreude. ;-)

>   I am
> curious about how the Coq community sees Lean. Does it see Lean as
> "competitor" of Coq? Is it possible for Coq to bridge the gap betweem
> interactive and automated theorem proving like Lean aims to do?
>
> Saulo

I think many Coq users are also familiar with, perhaps even regular 
users of, alternative dependent-typed proof assistants, such as Agda, 
Idris, F*, Matita, NuPrl, ATS2, etc.  I doubt many would see these as 
"competitors".  More like kin.

As for this "bridge the gap between interactive and automated theorem 
proving" - I'm not sure what the author(s) meant by this. Do they mean 
that Lean supports connections to various SMT solvers? Do they mean it 
has a powerful proof search capability?  Version 8.5 of Coq has 
considerably more proof search capability than did version 8.4, by 
virtue of its enhanced support for backtracking.  If that is what is 
meant by this "bridging the gap", then Coq perhaps qualifies.

-- Jonathan