Let me also recommend any interested in theorem proving check out ACL2. It is based on lisp and might be easier to get started with than Coq. There is a pretty cool website that lets you run it in a browser here along with a basic tutorial:

http://tryacl2.org/