Start with the one with the best documentation. It's hard to beat Software Foundations: https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.c

Start with the one with the best documentation. It's hard to beat Software Foundations: https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/, which happens to be for Coq. If you search the web for "Software Foundations in X", you will find partial ports of some of the initial chapters to pretty much any other proof assistant. Maybe nowadays they are full, complete ones that would allow you to use Isabelle or Lean instead.