最近集合論を形式化したノート作ったんだけど、せっかくだからプルーフチェッカーにでも通して遊んで
みたいんだけど、個人的に遊べるソフトはどれがお勧めですか？

今、MIZARとか言うのを解読中なんですが、HIDDEN.VOCが見当たらないんだよねえ。関数記号とかも
自分で定義したいんだけど、そういうのはＭＩＺＡＲには向いてないのかなあ。

もっとグラフィカルでわかりやすいのがあるといいなあ。