まえがき

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