压缩就是您所需要的：数学建模

arXiv:2603.20396v1 公告类型：新 摘要：人类数学（HM）是人类发现和重视的数学，是形式数学（FM）的一个极其小的子集，而形式数学是所有有效推论的总和。我们认为 HM 的特点在于其通过分层嵌套定义、引理和定理的可压缩性。我们用幺半群来建模。数学推导是一串原始符号；定义或定理是命名的子字符串或宏，其使用会压缩字符串。在自由阿贝尔幺半群 $A_n$ 中，对数稀疏宏集实现了表达能力的指数扩展。在自由非阿贝尔幺半群 $F_n$ 中，即使是多项式密集的宏集也只能产生线性展开；超线性膨胀需要接近最大的密度。我们针对 MathLib 测试这些模型，MathLib 是一个大型 Lean~4 数学库，我们将其作为 HM 的代理。每个元素都有一个深度（定义嵌套层）、一个包装长度（其定义中的标记）和一个展开长度（完全展开所有引用后的原始符号）。我们发现展开长度随着深度和包裹长度呈指数增长；缠绕长度在所有深度上大致恒定。这些结果与 $A_n$ 一致，但与 $F_n$ 不一致，支持 HM 占据指数增长空间 FM 的多项式增长子集的论点。我们讨论了在 MathLib 依赖图上测量的压缩以及该图的 PageRank 式分析如何量化数学兴趣并帮助将自动推理引导到人类数学所在的可压缩区域。