The Coq mailing list

[Ramkumar Ramachandra <artagnon AT gmail.com>]

Lean has much lower startup-cost for pure mathematicians, since the built-in features and mathlib are great for doing undergraduate-level group theory & topology, masters-level commutative algebra & category theory, but I think it plateaus quickly thereafter; future releases of Lean will probably fix this.

Lean seems to have taken a top-down approach, by focusing on writing real proofs as quickly as possible, without compromising soundness [https://github.com/digama0/lean-type-theory/releases/tag/v1.0]. There are three axioms in Lean: propositional extensionality, quotient soundness, and choice; however, these don’t block computation, since computation is done by a VM. However, they break good type theoretic properties like strong normalization, subject reduction, and canonicity — this was a conscious design choice, and they decided that these properties weren’t as important to working mathematicians.

Coq, on the other hand, has always been very particular about sound type theoretic foundations. The recent “Coq Coq Correct!” paper [https://www.irif.fr/~sozeau/research/publications/drafts/Coq_Coq_Correct.pdf] proves various metatheoretic properties of the Coq engine.

Lean supports both constructive and classical reasoning, but I’m hoping HoTT will be integrated into mainline Coq and solve most of the setoid-related issues (not that I understand much about it).

One would think that Lean is an engineering feat, since it’s written in C++ (and lean4 is written mostly in C): math-comp is 90k loc, while mathlib is 150k loc; and it takes over thirty minutes to build mathlib! Coq is much faster.

Quotients are indeed a great feature to have, and makes formalizing commutative algebra painless; an example [https://github.com/leanprover-community/mathlib/blob/master/docs/tutorial/Zmod37.lean] of using quotients in Lean. However, quotients are tricky to implement without breaking certain metatheoretic properties that Coq’ers cherish, which is why it hasn’t been implemented yet.

Lean’s inheritance [https://leanprover.github.io/theorem_proving_in_lean/structures_and_records.html#inheritance] is another good feature; it disallows diamond-inheritance, and seems like a bit of a hack, but Coq should definitely get some form of a well-thought-out ad-hoc polymorphism.

Category theory in Lean has not been developed [https://github.com/leanprover-community/mathlib/blob/master/docs/theories/category_theory.md] with higher categories in mind; I’m not sure how one would define ∞-categories, since universes are explicit, and since there are no coinductive types: Coq’s impredicativity seems to be a better design choice.

Footnote. Metamath Zero [https://github.com/digama0/mm0] might be of interest to the Coq community for high-performance checking.

Ram