Mizar Mathematical Library (MML) による ミザールの記事 構成、以下の 2 つの記事がこのデータセットの基礎となります。

• 組み込まれた概念
• タルスキー・グロタンディーク集合論の公理

Mizar Mathematical Library (MML) は、Mizar 言語に基づく数学的形式化ライブラリであり、多くの作成者や保守者によって長年にわたって構築されてきました。 Mizar 言語は、数学の定理、証明、および関連する概念を記述するために使用されるコンピューター可読言語です。 Mizar 数学ライブラリには、論理、代数、解析、幾何学などの幅広い数学分野をカバーする、形式化された数学の定理と証明が含まれています。このライブラリの目標は、自動化された定理証明と形式的推論のための強固な数学的基盤を提供することです。これまでのところ、ミザール言語システムは巨大なミザール数学ライブラリを形成しており、数学と関連問題の将来の議論のための良い基盤を築いてきました。