Classification and Dependency Visualization of the Articles of the Mizar Mathematical Library

EasyChair Preprint no. 10788

Abstract

The Mizar Mathematical Library (MML) is a collection of mathematical documents formalized by the Mizar system. Visualizing the interrelationships among the MML articles can illuminate their structure and connections, but the scale and intricacy pose significant challenges. In our research, we introduce a method to illustrate these MML dependencies: we sort the MML articles according to the classifications in the Encyclopedic Dictionary of Mathematics. Moreover, we are exploring the feasibility of utilizing generative AI to automate this sorting process, aiming to lessen the need for manual labor. Finally, we also discuss a new algorithm for rendering categorized dependency graphs.

Keyphrases: automated classification, ChatGPT, compound graph layout, Encyclopedic Dictionary of Mathematics, Mathmatics Subject Classification (MSC), Mizar, Mizar Mathematical Library (MML)

@Booklet{EasyChair:10788,
  author = {Shotaro Suzuki and Masahiro Nagasaki and Kazuhisa Nakasho},
  title = {Classification and Dependency Visualization of the Articles of the Mizar Mathematical Library},
  howpublished = {EasyChair Preprint no. 10788},

  year = {EasyChair, 2023}}