Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal Proofs

Formalization libraries for interactive theorem provers are rapidly growing in size, but only little is understood structurally about those developments. We aim to address the arising challenges by utilizing dependency graphs of the underlying formal entities. For the Isabelle Archive of Formal Proofs, the individual entry graphs consist of 1.8 million nodes and 2.8 million edges in total, and exhibit certain complex network characteristics: Node in-degrees weakly follow scale-free distributions with an average exponent of $$\alpha =1.81$$ , and the high clustering coefficient (avg. 0.33) together with the short average path length (3.64) indicate small-world effects. We did not find network centrality metrics to be good indicators of theory quality (measured by lint frequency): The Spearman correlation of our six different centrality metrics was weaker than in similar experiments from software systems, and with a coefficient of $$s=0.38$$ , the source lines of code metric exhibited a stronger correlation than all centrality metrics considered. In contrast, network centrality metrics worked well in predicting the most important concepts within AFP entries: Of the definitions deemed most important by entry authors, 51.7% could be identified at a precision of 27.7% (optimal $$F_1$$ -score), using in-degree centrality. At the cost of a few percentage points of precision, a second maximum of 68.8% recall can be achieved.