1. 21

  2. 2

    “Cultural chasm” seems like hyperbole when it comes to discussing the differences between these two tools.

    1. 12

      Both are based on pCIC, but there is a huge cultural difference: Coq focuses on sound type theory, while Lean focuses on writing proofs conveniently without worry too much about type theory. I wanted to highlight this.

      1. 2

        Thanks for clarifying.