Geometric Structure in the Lean 4 Mathlib Knowledge Graph

Formal mathematical libraries are scientific knowledge graphs whose vertices are definitions, theorems, lemmas, and constructions, and whose edges encode machine-checked logical dependency. This paper studies theLean 4 Mathlib library as such a knowledge graph. We construct a dependency graph with 619518 declarations and 12.5 million direct dependencies, and measure its large-scale and local geometric structure. The graph exhibits two different behaviours. At large scale, sampled four-point measurements indicate low Gromov hyperbolicity: the maximum observed value over 10000 sampled quadruples is delta=1.50 for the full graph and delta=1.00 after pruning the top 1% of vertices by degree. At local scale, a Jaccard-overlap proxy for Ollivier-Ricci curvature, evaluated on 20,000 sampled edges, has positive mean value k ~ 0.022. Thus the graph is globally thin but locally dense. We call this empirical pattern a tree-of-cliques structure. To test whether it is explained by graph size, degree distribution, or pruning, we compare Mathlib with three null models: an Erdos-Renyi graph, a Barabasi-Albert graph, and a configuration model preserving Mathlib's exact degree sequence. Under identical pruning, all three null models have negative mean local curvature under the same proxy. As a further control, we compare two independent formalizations of the same sphere-packing development, one human-written and one autoformalized, and find that both exhibit the same positive local curvature. This indicates that the effect is not an effect of human API design. Finally, we train a 16-dimensional Poincare ball embedding of the dependency graph and use it as an attention-allocation mechanism for knowledge discovery inside the library. Two Lean 4 case studies are presented: a reusable normalization lemma for tau-packings in a Besicovitch covering development, and the cycle matroid as a missing bridge between the SimpleGraph and Matroid namespaces. The results suggest that geometric analysis of formal-library knowledge graphs can support mathematical knowledge management, library assessment, and discovery of missing formal abstractions.