As someone who’s never messed with a theorem prover but would like to, would it make sense to start with Lean? How is it different from Coq? And is Coq worth learning before Lean?
It has improved a lot but still I think Lean has many things going for it including a large focus on programming and using your Lean programs directly (versus extraction, which is roughly a really shitty compiler from Coq to Ocaml or another extracted language).
Coq has FRAP and CPDT [1], which teach you most techniques that are used in industry. Also Software Foundations.
AFAIK, there's a version of Concrete Semantics using Lean [2]. But that's still just semantics.
Any other materials focused on software verification, not on formalizing mathematics?
It will blow your mind.