Lean versus Coq: The cultural chasm

submited by
Style Pass
2023-09-18 04:00:04

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.

Leave a Comment