Mizar
システムの開発は1973年にアンジェイ・トリブレッツによって始められ、システムの保守をポーランドのビアリストーク大学(英語版)、カナダのアルバータ大学、日本の信州大学で行っている。
Mizar-言語で記された証明文(以下、Mizar-論文)は普通のASCIIコードで書かれている。Mizar-言語は、数学の通常の言葉遣いと書式がよく似ており、数学者ならばMizar-論文を容易に読むことができる。また、証明を自動的に検証可能とするほど十分に形式化されたものである。Mizar-論文における証明の各段階は非常に自明なものである必要があり、そのため同等の内容を持つ通常の数学論文に比べ、長さにおいて4倍程度になると評価された。
Mizarの証明検証プログラムはPascalでかかれ、古典論理を用いた証明を行うもので、非商用目的であれば無料でダウンロード、利用が可能である。これはPC/AT互換機上のWindows、Solaris、FreeBSDおよびLinuxで、あるいはmacOS / Darwinで動く。ソースコードはMizar -ユーザ協会のメンバーだけが入手できる。