Mizar Mathematical Library (MML) 由 Mizar Articles 构成，以下两篇文章构成了该数据集的基础。

• built-in notions
• the axioms of the Tarski-Grothendieck set theory

Mizar 数学库 (Mizar Mathematical Library, MML) 是一个基于 Mizar 语言的数学形式化库，它是由许多作者和维护者多年建造而成的。 Mizar 语言是一种用于描述数学定理、证明和相关概念的计算机可读语言。 Mizar 数学库包含了经过形式化的数学定理和证明，涵盖了广泛的数学领域，包括逻辑、代数、分析、几何等。这个库的目标是提供一个可靠的数学基础，以便进行自动化的定理证明和形式化推理。目前为止，Mizar 语言系统已形成一个庞大的 Mizar Mathematical Library，它为今后讨论数学及其相关问题奠定了一个良好的基础。