Proof Generalのアイコン

次の次のマルレクで、数学の証明にコンピュータを使う「証明支援システム」の話をしようと思っている。

この分野、しばらくご無沙汰していたので、VoevodskyのプロジェクトUniMath ( https://github.com/UniMath/UniMath )をスクラッチからインストールした。

coqide の他にも、EMACSをインターフェースに使う Proof General と言うのもあるよと書いていたので、やってみて、EMACSを開いたら、最初に出てきたのがこの画面。ちょっとびっくり。

思わぬところでオタクをみつけた。これ、日本のカルチャーの影響だよね。日本、ある意味、スゴイのかも。Contributorに日本人の名前は見つけられなかったけど。（それでいいのかな？）

面白そうなので、触ってみたが、僕、vi派だったので、EMACS苦手なんだ。