Chapter 1
Mizarの概要
Mizar とは，ワルシャワ大学（ポーランド）の Andrzej Trybulec先生を中心とした Mizar Society によってすすめられている，数学をコンピューターを使って形式化するプロジェクトの総称です．Mizarプロジェクトは，コンピュータを使って数学を記述するために作られた Mizar言語によって数学の証明を記述し，それを IBM-PC 上で動作する Mizarプルーフチェッカーによってチェックし，それを Mizarライブラリに登録することによって行われます．このプロジェクトの目的は数学の論文のチェックのシステムを作ることです．
Mizarでは，数学の証明を記述したテキストのことを articleといいます．新たに article を書くときには，すでにチェックされていて Mizarライブラリに登録されている多くの article を参照することができます．そして，その article がいずれ Mizarライブラリに登録されたときには，それを他の article が参照することもできます．
article は，環境部（environ），本体部（text proper）に分かれており，環境部では，その article に必要な様々な環境設定を記述し，本体部では証明自体を記述します．
article は Mizar言語によって記述します．Mizar言語は，数学の一般的な証明の記述のしかたをもとにしていますが，Mizar独特の書き方もあり，これについては後で詳しく説明します．
ここでは Mizar言語，Mizarプルーフチェッカー，さらに Mizarプロジェクトについて説明します．