As an amateur, I have heard differing opinions on this topic, but I quite enjoyed working through the "Software Foundations" book: https://softwarefoundations.cis.upenn.edu/.

This book uses the Coq proof assistant to work through simple example proofs. If you stick with it for a while, the puzzle of finding proofs and getting instantaneous feedback from the assistant becomes quite an enjoyable process.