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 prett

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/ http://tryacl2.org/