Mizar Mathematics Dataset

Mizar Mathematical Library (MML) by Mizar Articles Composition,The following two articles form the basis of this dataset.

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

Mizar Mathematical Library (MML) is a mathematical formalization library based on the Mizar language, which has been built over many years by many authors and maintainers. Mizar language is a computer-readable language for describing mathematical theorems, proofs, and related concepts. The Mizar Mathematical Library contains formalized mathematical theorems and proofs covering a wide range of mathematical fields, including logic, algebra, analysis, geometry, etc. The goal of this library is to provide a reliable mathematical foundation for automated theorem proving and formal reasoning. So far, the Mizar language system has formed a huge Mizar Mathematical Library, which has laid a good foundation for future discussions of mathematics and related issues.