The Coq mailing list

[Freek Wiedijk <freek AT cs.ru.nl>]

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