The Coq mailing list

[Théo Zimmermann <theo.zimmermann AT ens.fr>]

Hi Freek,

Lean has two modes: one standard and one "HoTT". The standard one has proof irrelevance built-in, indeed, but the HoTT one has not, of course. Leonardo de Moura claims that Lean would make it possible to add new modes, if a new logic became of much interest for experimentation.

As for bridging the gap between automated theorem proving and interactive theorem proving, this is a long term goal. Leonardo de Moura comes from the world of automated theorem proving so has probably some interesting plans on how to do so.

On how it compares to Agda and Coq, I would add that by default you write your proofs as terms, but these terms look more natural, by the use of keywords such as take and assume instead of fun; and have. There is also a tactic mode which you can easily switch to (similar to Coq's new tactic in term capability).

Théo

Le jeu. 25 févr. 2016 à 12:01, Freek Wiedijk <freek AT cs.ru.nl> a écrit :

Hi Jonathan,

>It looks eerily similar to Coq.

I also is quite different from Coq in some respects.

It is implemented in C++, not in ML.  It has proof
irrelevance, function extensionality, classical logic, even
a choice operator as part of the standard setup (exactly
which of those are hardwired in, and which ones are just
conventionally available in the library, I don't know.)
It has been explicitly designed to be useful for HoTT (how
that can be true in conjunction with the previous sentence, I
don't know :-))  The type theory is simpler: they don't have
"match" in the foundations, but instead work with recursors,
and they don't have universe cumulativity.

Jeremy Avigad is one of the people behind Lean.  He comes
from an Isabelle background.  I can imagine Lean will feel
more familiar to Isabelle people than Coq does.

Freek