I spent a 6 month parental leave learning it and experimenting with it. I enjoyed writing specifications so much that I thought programming was a waste of time. You should watch the video lectures. The first 2 or 3 will get you going. A first simple exercise might be to specify the least common multiple following Lamport's GCD example.
I'm a math major, by the way.