数理論理の2科目が終わった。院生の研究テーマにされることもあるというMizarについて、いくつかアナウンスがあったのでちょっと見てみたり。

http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/index-j.html

数学の証明を記述し計算機によって数式を解いたりするものであろう。ちょうど数理論理をやった後なので、何をするものか多少読める気はする。
まぁ、しかしこれはこれ。