If you want a gentle introduction you may like this book http://the-little-prover.github.io/