最近 Anarchy Proof に熱中しています。 kikxさんによる、 Anarchy Golf リスペクトな 「ユーザが好き勝手に定理を投稿するのでみんなで証明を書いて競おう！」 的なサイトです。
定理や証明の記述には（今のところ？） Coq というシステムを使います。 Coq については、2008年の LL Future の LT であった 超未来言語 Gallina という発表などをどうぞ。 （Gallina というのは Coq の中で使うプログラミング言語の名前で、 つまり昔の "Object Pascal" と "Delphi" みたいな関係。） 他にも検索すれば解説が結構見つかるはず。
Coq や Agda みたいな「証明の書けるプログラミング言語」は使いこなせるようになりたいなー、 と常々思っているのですが、 なかなか適度な練習問題がなくて、 どこから手をつけたらいいかわからない、 という状況だったので、 単純に問題集としてありがたいなー、 と思いながら挑んでいます。 みんなもこれで Coq マスターになろう！
あとそういえば、 今月末に名古屋で Coqのイベント があるそうです。 ペアプルービング！