3 ms·
Opinion, but lean and coq both use dependant type theory, while isabelle uses a first order logic. Between coq and lean, lean has always had great support for u
by ratmice 2y ago
Opinion, but lean and coq both use dependant type theory, while isabelle uses a first order logic. Between coq and lean, lean has always had great support for unicode, where coq always seemed to me ascii first, and coq itself predates the publishing of the unicode standard and formation of the unicode consortium. At least my feeling has always been that syntax probably takes no small part in it. Because with lean one can use all the familiar mathematical alphanumeric symbols and operators.
- robinzfc 2y agoIsabelle is a generic theorem prover. It supports the standard set theory on first order logic as well, but it's most popular logic is HOL, which is a kind of type theory. Isabelle is well integrated with LaTeX, so its support for mathematical symbols goes beyond unicode. One can write complete well typeset mathematical papers inside Isabelle, and people do. So it's not that. Yet, the dynamics of Lean uptake among mathematicians is much better, so I am curious why is that. I would really like to see an opinion of someone who knows both Lean and Isabelle well, but prefers Lean for formalized mathematics. Or is that all coincidence and hype?
- ratmice 2y agoI am talking not about the ability to typeset your proofs, but the source code itself for the proofs. At the very least all the Isabelle and Coq proofs I've looked at have look much more like source code than the proofs they formalize.