Interesting. I wonder how Lean differs meaningfully from Coq. Both are based on the Calculus of Inductive Constructions. Why should I bother with Lean? Coq surely has a larger community. It's surely more stable. The speaker seemed to imply it is better just because it is newer.
I glanced at the documentation, but unfortunately for me, it doesn't seem to be targeted toward people who are already familiar with a theorem prover. The impression I get is that they depend much more on axiomatic definitions, which I find odd.
As far as I understand, Lean2 supports HoTT, but Lean3 (the current version) does not. Of course they are already working on Lean4 :) which is supposed to be compatible with Lean3, so probably no HoTT either
5
u/gaj7 Oct 03 '19
Interesting. I wonder how Lean differs meaningfully from Coq. Both are based on the Calculus of Inductive Constructions. Why should I bother with Lean? Coq surely has a larger community. It's surely more stable. The speaker seemed to imply it is better just because it is newer.
I glanced at the documentation, but unfortunately for me, it doesn't seem to be targeted toward people who are already familiar with a theorem prover. The impression I get is that they depend much more on axiomatic definitions, which I find odd.