Coq
Earlier this week I started to learn Coq, the proof assistant. I was able to get going in just a few hours of monkeying around—it's clearer and easier to use than I expected, and much more pleasant than previous stabs at Isabelle and the like. My advice to Coq learners is to sit down with the IDE, the tutorial, and the tactics index. Using it is largely a matter of throwing different tactics at the proof until they seem to give you some progress. Of course, having a measure of mathematical and logical reasoning helps, too.
By the end of the first half-day of tinkering with it, I was able to show that every lambda-term has a variable as a subterm. Doesn't sound too impressive, but when you see those nice lemmas and their proofs all written out and mechanically checked, you get a feeling of goodness on your insides. Plus, the hours I played with it just slipped away (though whether that's a good quality or a bad one is debatable). You heard it here first, folks, Ezra elias kilty Cooper gives Coq the thumbs up.