[agentultra]

As far as theorem provers go Coq seems to be the most widely known among working programmers.

Lean deserves wide recognition. First, it's fast enough for highly interactive theorem development. Second it can also be used as a programming language. And lastly its syntax is pleasant to work with which is important to the experience.

If you have only heard about interactive theorem provers and don't yet have any opinions I'd give Lean a try first. The interactive tutorials are nice and the aforementioned features make it pleasant to work with.

[tathougies]

These are interesting pros for lean. I just wanted to point out that Coq is also a programming language, and there are some packages of hackage of various data structures proven correct in Coq and then compiled from the original coq sources.

[agentultra]

I have read a fair bit about use of hs-to-coq and coq-haskell; Coq is a nice tool for sure!

[benwr]

Strongly agree. I only found Lean after a couple of weeks of struggling to pick up coq. In my opinion, this tutorial alone makes lean a better choice for beginners.

[tom_mellior]

Out of interest, what about this tutorial do you find better than (which?) Coq tutorials?

I think Lean might be the better technology, but I don't think this tutorial is better than Software Foundations. I can't see beginners not being turned off by boring discussions of hierarchies of universes before the first real proofs to get you hooked.

[benwr]

This tutorial starts by explaining how things work, and only later shows you magic. That's exactly what I like about it, actually. Almost every coq tutorial I found (I tried software foundations, cpdt, and several shorter online tutorials) fails to explain what you're doing before you do it.

[tom_mellior]

Fair enough. That's not my preferred approach to tutorials, but tastes differ. Thanks.

[elcapitan]

What's the upside compared to coq?