News for hackers. Stuff that matters.

A comment on Theorem Proving in Lean. Parent comment

Re:Theorem Proving in Lean by gmfawcett on Tuesday May 29, 2018 @11:04AM (#17179754)
Cool, thanks for this. I've yet to play with Lean, but it looks very interesting! (I'm hoping that my time invested in Coq will transfer reasonably well...)
[ Parent | on HN ]
Re:Theorem Proving in Lean by tom_mellior on Tuesday May 29, 2018 @03:32PM (#17182250)
You're welcome! I'm in a similar boat, coming to this tutorial from a Coq background (and some Isabelle/HOL). I'm pleasantly surprised how similar many things are. But I'm also a bit disappointed because I was under the impression that Lean was relying on automation via Z3 a lot more. Not quite done with the tutorial yet, so there might still be some material to this effect coming up, but I'm afraid not.
[ Parent | on HN ]