The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Yes, Jeremy's Isabelle background can be seen too. The proofs are,
arguably, more readable than Coq proofs.

The lean tutorial gives a good overview of the system.

On Thu, Feb 25, 2016 at 12:01 PM, Freek Wiedijk 
<freek AT cs.ru.nl>
 wrote:
> 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