人类数学（HM）——即人类所发现并重视的数学——仅仅是形式数学（FM）这一庞大体系中一个微乎其微的子集；而形式数学则囊括了所有有效的逻辑推导。我们认为，人类数学之所以独特，在于它可通过层级嵌套的定义、引理与定理实现高度压缩。我们采用幺半群（monoid）对这一特性建模：一条数学推导可表示为一串原始符号构成的字符串；而一个定义或定理则相当于一个被赋予名称的子串（或称“宏”），其引入可显著压缩该字符串的长度。在自由阿贝尔幺半群 $A_n$ 中，即便仅采用对数稀疏（logarithmically sparse）的宏集合，亦足以实现表达能力的指数级扩展；而在自由非阿贝尔幺半群 $F_n$ 中，即使宏集合的密度达到多项式级别，所能获得的表达能力提升也仅为线性；若要实现超线性扩展，则宏集合的密度必须接近最大可能值。我们以 MathLib（一个规模庞大的 Lean 4 数学形式化库）作为人类数学（HM）的实证代理，对上述模型展开检验。MathLib 中每个数学对象均具有三个关键度量：深度（即定义嵌套的层数）、包裹长度（其定义所含的词元 token 数量）以及展开长度（将其中所有引用完全递归展开后所得的原始符号总数）。我们发现：展开长度随深度与包裹长度均呈指数增长；而包裹长度则在各深度层级上大致保持恒定。这些经验结果与自由阿贝尔幺半群 $A_n$ 的理论预测高度吻合，却与自由非阿贝尔幺半群 $F_n$ 的预测明显相悖，从而支持如下核心论断：人类数学（HM）占据着形式数学（FM）这一指数级增长空间中一个仅呈多项式级增长的子区域。最后，我们进一步探讨：如何借助 MathLib 的依赖图（dependency graph）来量化“数学重要性”——具体而言，既可通过该图上的压缩率（compression ratio）加以衡量，也可通过类比 PageRank 的图分析方法进行评估；此类量化手段不仅能揭示哪些数学内容更富“兴趣”，还可引导自动化推理系统聚焦于那些具备强压缩性的区域——而这恰恰正是人类数学赖以生存与繁衍的土壤。
