[sevensor]

I've got very little experience with theorem provers, but I have spent some time working through this book, and I can recommend it. If you're interested, the Emacs Lean mode works great.