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%；第三，形式化过程压缩了语义层级，网络中心性反映的是语言基础设施而非数学相关性。