1. 14

I’ve been finding this a really great intro to automated theorem proving and dependent types, after having wandered for a week or so in the wilderness that is Coq tutorials and books.

  1.  

  2. 5

    Lean is awesome :) An Introduction to Lean is a nice (albeit incomplete) one too.

    There’s a fairly active community on Zulip over at https://leanprover.zulipchat.com if you like to drop by for a chat or get some help.