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.
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.
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.