Mizarは証明検証系です。形式的な証明記述言語とその処理系という括りではCoqやIsabelleの仲間ですが、対話的ではないので使い勝手はだいぶ違います。とりあえずインストールして使ってみましょう。内容： インストール 使ってみる 感想 インストールMizarの…