HyperAI超神经

Mizar 数学数据集

日期

1 年前

发布地址

mizar.org

许可协议

CC BY 4.0

下载帮助

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

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