Lean versus Coq: The cultural chasm

Last updated: Saturday, 04 January 2020

Lean has much lower startup-cost for pure mathematicians, since its built-in features and [math library](https://github.com/leanprover-community/mathlib) are great for doing undergraduate-level group theory & topology, masters-level commutative algebra & category theory, but it plateaus quickly thereafter.

Lean seems to have taken a top-down approach, by focusing on writing real proofs as quickly as possible, without compromising on [soundness](https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf). There are three axioms in Lean: `propositional extensionality`, `quotient soundness`, and `choice`; however, these don't block computation, since computation is done in a VM. They do, however, break good type theoretic properties like `strong normalization`, `subject reduction`, and `canonicity` — this was a conscious design choice.

Coq, on the other hand, has always been very particular about sound type theoretic foundations. The recent ["Coq Coq Correct!"](https://www.irif.fr/~sozeau/research/publications/drafts/Coq_Coq_Correct.pdf) formalizes the Coq engine proving metatheoretic properties about it, in Coq, and [HoTT](https://github.com/HoTT/HoTT) is being actively developed to fix many of Coq's issues.

Working mathematicians have only just started using software for their work, and they often rely on unverified (and sometimes proprietary) tools like magma, sage, and mathematica. Lean is a big step-up, and the good type theoretic properties preserved by Coq don't seem as important to them.

Lean supports both constructive and classical reasoning, but classical reasoning in Coq is painful due to ["setoid-hell"](http://www.cs.nott.ac.uk/~psztxa/talks/types-17-hell.pdf); something that would be fixed by the HoTT line of work.

[Quotient-reasoning](https://github.com/leanprover-community/mathlib/blob/master/docs/tutorial/Zmod37.lean) makes formalizing commutative algebra painless, and it's baked into the Lean kernel. However, quotients are tricky to implement without breaking certain metatheoretic properties that Coq'ers cherish; nevertheless, there is an [implementation](https://math-comp.github.io/htmldoc/mathcomp.ssreflect.generic_quotient.html) in Coq's [math-comp](https://github.com/math-comp/math-comp), albeit, without a reduction rule.

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 is definitely missing 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 $\infty$-categories, since universes are explicit, and since there are no coinductive types: Coq's impredicativity seems to have been a better design choice.

One would think that Lean is an engineering feat, since it's written in C++ (and Lean4 is written mostly in C): Coq's math-comp (90k loc) compares to Lean's mathlib (150k loc); math-comp builds in under ten minutes, while mathlib takes over thirty minutes to build! Indeed, due to their design decision to use a VM for computations, computation happens at a speed comparable to Python-bytecode evaluation — they seem to be overhauling this in Lean4 though, by compiling Lean code down to C before execution.