3 ms·

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 les

by srl 5y ago

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.

mbrodersen 5y ago
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).