  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.
