Lean versus Coq: The cultural chasm

Both Lean and Coq are proof assistants based on pCIC. Here, we argue that what sets them apart are, in essence, cultural differences.

Lean has much lower startup-cost for pure mathematicians, since its built-in features and math library 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. 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!" formalizes the Coq engine proving metatheoretic properties about it, in Coq, and 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 quotienting in Coq is painful due to "setoid-hell"; something that would be fixed when types are modeled as -groupoids instead of setoids, as in the HoTT line of work.

Quotient-reasoning 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 in Coq's math-comp, albeit, without a reduction rule.

Lean's 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 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 cumulativity seems to have been a better design choice.

One would think that Lean is an engineering feat, since it's written 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.

Another reason for the relative slowness of Lean is that they do a lot of automation under the hood, figuring out, for instance, that when the user writes , and are topological spaces, and that here means product topology.