Mizarとはなんですか？

ページ名：Mizarとはなんですか？

A. 自動証明検証システム Mizarは、数学的な定義や証明を厳密に形式的に記述するためのデータ記述言語、証明検証プログラム、ライブラリから構成されるシステムです。