The effort required for maintaining large libraries of formal mathematics is quite substantial. In this work, we exploit structural similarity to alleviate the burden of maintenance, investigating two main problems: First, we present a general framework for detecting duplicates in large libraries of formal mathematics, combining surface-level syntax, document markup, and the underlying formulae. For scalability, we generate potentially matching candidates with a discriminator-based approach. On Isabelle/HOL, our method maintains perfect precision up to a similarity threshold of 0.95. Secondly, we address the issue of out-of-place auxiliary lemmas that are frequently created during development of in-depth formalizations. We propose a community detection approach on the underlying dependency graph of formal entities, which finds co-located lemmas that have similar link patterns. For a dataset of lemmas moved during Isabelle development, the correct location is in the top 6 neighborhoods suggested by our approach on average (median).