mizar-items: Exploring fine-grained dependencies in the Mizar Mathematical Library

TL;DR

This paper introduces mizar-items, a system for decomposing the Mizar Mathematical Library into fine-grained items and analyzing their dependency relations, facilitating foundational research in formalized mathematics.

Contribution

The paper presents a novel method for fine-grained decomposition and dependency analysis of the Mizar Mathematical Library, enabling detailed exploration of mathematical dependencies.

Findings

Decomposes MML into detailed items like theorems and definitions.

Computes dependency relations among fine-grained items.

Provides an interactive website for dependency exploration.

Abstract

The Mizar Mathematical Library (MML) is a rich database of formalized mathematical proofs (see http://mizar.org). Owing to its large size (it contains more than 1100 "articles" summing to nearly 2.5 million lines of text, expressing more than 50000 theorems and 10000 definitions using more than 7000 symbols), the nature of its contents (the MML is slanted toward pure mathematics), and its classical foundations (first-order logic, set theory, natural deduction), the MML is an especially attractive target for research on foundations of mathematics. We have implemented a system, mizar-items, on which a variety of such foundational experiements can be based. The heart of mizar-items is a method for decomposing the contents of the MML into fine-grained "items" (e.g., theorem, definition, notation, etc.) and computing dependency relations among these items. mizar-items also comes equipped with a website for exploring these dependencies and interacting with them.