Из блога Терренса Тао узнал, что есть такая логическая игра QED или по-другому можно назвать интерактивный учебник логики.
Рекомендую всем, кому больше 10 лет и кто интересуется theorem prover-ами.

P.S.
Для игры (и для работы с theorem prover-ами тоже) полезно знакомство с Natural deduction Генцена. К сожалению сейчас не вспомню, где об этом хорошо написано по-русски.