MMLKG: Mizar Mathematical Library Knowledge Graph

MMLKG is a thesaurus for describing a repository of computer-verified mathematical papers written in the Mizar language. The dataset includes a GraphML file for loading into graph databases, CSV relationship files, and RDF data. It was prepared by Dominik Tomaszuk and is available under an Open Access license.

Use Cases

• Constructing a knowledge graph of formal mathematics based on the Mizar Mathematical Library.
• Linking formal mathematical concepts to external resources like Wikidata and DBpedia using the provided RDF data.
• Analyzing relationships between theorems, definitions, and proofs within a computer-verified corpus.

Strengths

• Includes multiple file formats (GraphML, CSV, RDF) for different use cases.
• Links to external knowledge bases like Wikidata and DBpedia are provided.

Limitations

• Column-level documentation is absent; field semantics must be inferred after download.
• Row count is unknown, which may limit suitability assessment.
• Last update date is unknown; freshness unverified.

Provenance

Source

Mizar Mathematical Library

Collection Method

Derived from a repository of computer-verified mathematical papers.