If you're considering Coq but haven't started I'd also consider Lean[0]. The documentation isn't as great but the main tutorial is decent. It also doubles as a

If you're considering Coq but haven't started I'd also consider Lean[0]. The documentation isn't as great but the main tutorial is decent. It also doubles as a practical programming language. And the community is active and helpful. I've always found Coq to be a little impenetrable. I don't know what makes Lean more accessible to me but I've found it much easier to get into. [0] https://leanprover.github.io/ https://leanprover.github.io/