まえがき
Mizarは，もっとも有名なプルーフチェッカーの１つです．歴史的にはかなり古い方ですし，それから，本格的な数学用言語としてはいちばん完成度が高いものだということがいえると思います．プルーフチェッカー自体は世界中に何十種類とあるようですが，それらは大学院の学生が卒論でつくって，それでその学生が卒業したら誰も使わなくなってしまったようなものがたくさんあるわけです．その中にあって，Mizarはワルシャワ大学の Andrzej Trybulec先生を中心とした Mizarグループによって，多くの研究者や大学院生などがそれに協力してライブラリを増やしています．
Trybulec先生はもともとは数学者であるため，どんなプルーフチェッカーが必要であるかということをよく知っておられます．したがって，そういう経験をもとに作られましたので機能も充実していると思います．このプルーフチェッカーというものは，昔にはもちろんこういうものはなくて数学は非常に厳密な学問であると思われていました．多くの人が機械に頼るまでもないと思っていました．しかし，コンピュータの発達に伴って，その厳密さというものに疑問が感じられるようになってきました．そして，その数学をまずどういうふうに記述すべきかということが問題になったわけです．プルーフチェッカーは皆それぞれ考え方が違っています．私が作ったTHEAXもそのうちの１つですけれども，Mizarとはまったく独立に，時期的にはほとんど同じか，少しTHEAXの方が遅れてるかもしれませんが，ほぼ同じ頃に独立につくっています．したがって考え方がまったく違っています．
ここでは Mizarの考え方，どういう考え方で数学を形式化したかということの話，そしてまた実際の動作環境についても説明していきたいと思います．