Mizar
Mizarの配布物には、新たに書かれる Mizar-論文で参照可能な種々の定義および定理から成るMizar数学ライブラリ(Mizar Mathematical Library, MML)が含まれる。レビューと自動検証を受けた新たな論文は、形式化数学ジャーナルの関連刊行物で公表することができ、また然る後MMLの一部に組み込まれる。
MMLはタルスキー・グロタンディーク集合論の公理に基づいて構築される。2008年5月現在、8,800の定義と46,000の定理を含む。例えばハーン・バナッハの定理、ケーニヒの補題、ブラウワーの不動点定理、ゲーデルの完全性定理、カントール集合に関するいくつかの事実、などがMMLに含まれる。
MMLの扱う全ての対象は意味論的には集合である一方、Mizar-言語では統語論的な「型」を定義して使うことが許されている。例えば、ある変数が自然数を表すものならばNat-型を、群を表すならGroup-型を宣言することができる。このような記法は数学者にとっての記号の捉え方とより近く、Mizar-言語をより扱いやすいものにしている。
閲覧可能なMML-論文の概要は形式化数学ジャーナルのウェブサイトから入手できる。またMML QueryはMML-検索エンジンを実装している。