Structure in Theorem Proving: Analyzing and Improving the Isabelle Archive of Formal Proofs

TL;DR

This paper analyzes the structure of the Isabelle Archive of Formal Proofs, revealing scale-free properties in its dependency graph and discussing challenges and improvements in navigating and reusing large formal proof repositories.

Contribution

It provides an analysis of the archive's dependency graph structure and proposes methods to enhance accessibility and reusability of large theorem proving repositories.

Findings

Dependency graph node in-degree follows a scale-free distribution

Identifies challenges in finding and reusing material in large archives

Preliminary results suggest structural properties useful for improving archive usability

Abstract

The Isabelle Archive of Formal Proofs has grown to a significant size in the past years. It makes up for an impressive body of research, which enables a number of statistical approaches to various aspects in theorem proving, and has not yet been utilized exhaustively. However, the growing size also poses some challenges to address: Material becomes increasingly harder to find, reusability and ease of understanding become more important. This thesis abstract summarizes my research plans on those topics and briefly touches on preliminary results, which indicate that the node in-degree of the dependency graph of the archive follows a scale-free distribution.