Hacker News Reader

How does Lean compare to Coq? And which one would be preferable for non-mathematicians trying to learn more about math? Which one would be better if you come from a software background and want to do formal verification for parts of your programs?

View on HN

There's an excellent online book that introduces Coq and how to use it for verification of programs: https://softwarefoundations.cis.upenn.edu/. There's also a more advanced book, http://adam.chlipala.net/cpdt/, that goes into more detail. In comparison, Lean has little teaching material for formal verification of programs.

Thanks, that's very helpful!

You're welcome!

This is only a partial answer, but my understanding is that Lean is really not meant for software verification work. That's very much Coq's alley.

I'm much less certain of this, but I think Lean is better for non-mathematicians trying to learn more about math --- provided, that is, that you're set on playing with a proof assistant. I'm not sure I'd recommend that.

Not true. Lean and Coq are very similar. However it is true that Coq has more of a history when it comes to verifying software (CompCert is written in Coq for example). And Lean is the state of the art when it comes to mathematics (mathlib).

Reply on news.ycombinator.com