3 ms·

Lean has been going hard at PR at the moment. I would really like to dip my toe into the theorem proving waters from a scientific/mathematical perspective. I'

Lean has been going hard at PR at the moment. I would really like to dip my toe into the theorem proving waters from a scientific/mathematical perspective. I'm not sure whether to start with Coq, Agda, Isabelle or Lean. Does anyone on HN have a feeling as to a sensible one to start with?

zitterbewegung 7y ago
I have tried to use some of these theorem proving systems . Since Coq is pretty popular (which means lots of documentation and examples ) I would try that
tom_mellior 7y ago
Start with the one with the best documentation. It's hard to beat Software Foundations: https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/, which happens to be for Coq. If you search the web for "Software Foundations in X", you will find partial ports of some of the initial chapters to pretty much any other proof assistant. Maybe nowadays they are full, complete ones that would allow you to use Isabelle or Lean instead.
- phonebucket 7y ago
  Software Foundation and Coq looks like a fantastic resource. Thank you very much.
tel 7y ago
Coq is definitely the best documented. Unfortunately, the tendency to use the tactics language—while incredibly practically useful—obscures how the structure of proofs relate to their theorems. This isn't really a problem per se, but instead an invitation to look into, say, Agda to see that side of things, too.
- deleted 7y ago
  [deleted]
- zozbot234 7y ago
  Agda just uses proof terms directly - you could do that in Coq and Lean as well. It's a bit of a bummer though that neither Coq nor Lean have a currently-maintained declarative mode ala Mizar/Isar. The former C-zar included in older Coq versions (aka Mathematical Proof Mode) was especially nifty, albeit not totally free from bugs. (One other approach is to generate a "declarative", human-readable version of the proof directly from the proof term. Very old versions of Coq (6.x series) and IIRC even Agda (1.x) could essentially do this. Declarative proof mode integrates better with complex tactics however - proof terms can sometimes get a bit weird.)
  - tel 7y ago
    I agree that you can—I've done that in Coq, though I don't have any experience with Lean. The advantage of Agda is that everyone else does, too. This provides two things: one, there's a huge set of examples of how people have constructed their proof terms which encode best practices and are themselves designed to be as readable as possible, and two, people also build tooling which helps you to make them. In Coq, since tactics are primary, you end up with things like Sledgehammer. This is super practical and useful for tactics management, but it's a whole culture that will take you further and further away from understanding how proof terms work.
vilhelm_s 7y ago
Coq and Isabelle are much more mature systems, they have already been used in a lot of big developments, and they have large user communities and existing textbooks and so on. Agda is pretty finicky, proving stuff in it is harder and the entire project feels more researchy (as a playground to try out ideas for programming languages). Lean seems promising, but it's still kind of new, so compared to Coq will not find as much documentation, and there are fewer people on Stack Overflow to answer questions.

zitterbewegung 7y ago

I have tried to use some of these theorem proving systems . Since Coq is pretty popular (which means lots of documentation and examples ) I would try that

tom_mellior 7y ago

Start with the one with the best documentation. It's hard to beat Software Foundations: https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/, which happens to be for Coq. If you search the web for "Software Foundations in X", you will find partial ports of some of the initial chapters to pretty much any other proof assistant. Maybe nowadays they are full, complete ones that would allow you to use Isabelle or Lean instead.

phonebucket 7y ago
Software Foundation and Coq looks like a fantastic resource. Thank you very much.

tel 7y ago

Coq is definitely the best documented. Unfortunately, the tendency to use the tactics language—while incredibly practically useful—obscures how the structure of proofs relate to their theorems. This isn't really a problem per se, but instead an invitation to look into, say, Agda to see that side of things, too.

deleted 7y ago
[deleted]
zozbot234 7y ago
Agda just uses proof terms directly - you could do that in Coq and Lean as well. It's a bit of a bummer though that neither Coq nor Lean have a currently-maintained declarative mode ala Mizar/Isar. The former C-zar included in older Coq versions (aka Mathematical Proof Mode) was especially nifty, albeit not totally free from bugs. (One other approach is to generate a "declarative", human-readable version of the proof directly from the proof term. Very old versions of Coq (6.x series) and IIRC even Agda (1.x) could essentially do this. Declarative proof mode integrates better with complex tactics however - proof terms can sometimes get a bit weird.)
- tel 7y ago
  I agree that you can—I've done that in Coq, though I don't have any experience with Lean. The advantage of Agda is that everyone else does, too. This provides two things: one, there's a huge set of examples of how people have constructed their proof terms which encode best practices and are themselves designed to be as readable as possible, and two, people also build tooling which helps you to make them. In Coq, since tactics are primary, you end up with things like Sledgehammer. This is super practical and useful for tactics management, but it's a whole culture that will take you further and further away from understanding how proof terms work.

vilhelm_s 7y ago

Coq and Isabelle are much more mature systems, they have already been used in a lot of big developments, and they have large user communities and existing textbooks and so on. Agda is pretty finicky, proving stuff in it is harder and the entire project feels more researchy (as a playground to try out ideas for programming languages). Lean seems promising, but it's still kind of new, so compared to Coq will not find as much documentation, and there are fewer people on Stack Overflow to answer questions.