The ongoing development of Lean 4's Mathlib has produced a macroscopic structural complexity that interweaves logical, mathematical, and infrastructural dependencies. We present a network analysis of this library, extracting its dependency structure into a multilayer graph of 308,129 declarations, 8.4 million edges, and 7,563 modules. By introducing graph decompositions that isolate explicit edges from those synthesized by the compiler or driven by proofs, we quantify the structural properties of formalized mathematics. Our analysis reveals three findings. First, taxonomies designed by humans diverge from logical structures, exhibiting a 50.9% coupling across namespaces. Second, developers utilize a median of 1.6% of the imported scope. Third, formalization compresses semantic hierarchies, with network centrality capturing language infrastructure rather than mathematical relevance.

翻译：Lean 4的Mathlib持续开发产生了交织逻辑、数学与基础设施依赖的宏观结构复杂性。本研究对该库进行网络分析，将其依赖结构提取为包含308,129个声明、840万条边和7,563个模块的多层图。通过引入可分离显式边与编译器合成或证明驱动边的图分解方法，我们量化了形式化数学的结构特性。分析揭示三项发现：第一，人工设计的分类体系与逻辑结构存在偏差，命名空间之间呈现50.9%的耦合度；第二，开发者所用导入范围的中位值仅为1.6%；第三，形式化压缩了语义层级，其网络中心性反映的是语言基础设施而非数学相关性。