Mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library

摘要

The M M L is one of the largest collection of formalized mathematical knowledge that has been developed with various interactive proof assistants. It comprises more than 1100 "articles" summing to nearly 2.5 million lines of text, each consisting of a unified collection of mathematical definitions and proofs. Seman-tically, it contains more than 50000 theorems and more than 10000 definitions expressed using more than 7000 symbols.