3 ms·

What’s different about Lean compared to older theorem provers like Coq and Isabelle? I mean mathematicians could’ve used Coq / Isabelle / etc for decades for th

What’s different about Lean compared to older theorem provers like Coq and Isabelle? I mean mathematicians could’ve used Coq / Isabelle / etc for decades for the same purpose. Why didn’t they? What’s does Lean do differently that excites mathematicians and makes it more appealing?

yo_yo_yo-yo 2y ago
I think two primary things, which are connected. First, Kevin Buzzard, a “real” mathematician (as he self-identifies), promoted computer formalization of research mathematics with the Xena project, and second when looking for tools he latched onto Lean because he felt it more ergonomic. [1] He later discovered why Coq, Isabelle/HOL, and other tools did things in certain ways [2] (which were more “natural” to computer scientists) but by then his advocacy and inertia (the growing, curated MathLib) cemented Lean as the tool mathematicians tried first and sort of stuck with. [1] https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=21200721 [2] https://xenaproject.wordpress.com/2020/07/03/equality-specifications-and-implementations/ https://xenaproject.wordpress.com/2020/07/03/equality-specif...
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 ago
  Isabelle 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 ago
    I 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.

yo_yo_yo-yo 2y ago

I think two primary things, which are connected. First, Kevin Buzzard, a “real” mathematician (as he self-identifies), promoted computer formalization of research mathematics with the Xena project, and second when looking for tools he latched onto Lean because he felt it more ergonomic. [1] He later discovered why Coq, Isabelle/HOL, and other tools did things in certain ways [2] (which were more “natural” to computer scientists) but by then his advocacy and inertia (the growing, curated MathLib) cemented Lean as the tool mathematicians tried first and sort of stuck with. [1] https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=21200721 [2] https://xenaproject.wordpress.com/2020/07/03/equality-specifications-and-implementations/ https://xenaproject.wordpress.com/2020/07/03/equality-specif...

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 ago
Isabelle 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 ago
  I 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.