Mathematics is compression, and the compression ratio is measurable.
Analysis of MathLib — the Lean 4 mathematics library (arXiv:2603.20396). Every definition, lemma, and theorem is a macro: a named substring that compresses the text below it. Unwrap all macros — replace every name with its full definition, recursively — and measure the resulting length.
The finding: unwrapped length grows exponentially with depth and wrapped length, while wrapped (compressed) length remains relatively constant. A theorem that takes ten lines to state might take millions of characters to state without definitions. The compression ratio is not incidental — it's what makes the theorem possible to think, communicate, and verify. Without compression, the statement exceeds human (and machine) working memory.
The model uses monoid theory to formalize how macros expand expressivity. Abelian structures (where composition order doesn't matter) produce different expansion patterns than non-abelian ones. MathLib's actual expansion pattern fits the abelian model — suggesting that mathematical practice, as recorded in formal libraries, composes definitions in order-independent ways.
The practical application: compression analysis and PageRank on dependency graphs can identify where “human mathematics lives” in the space of possible formal statements. The highly compressed, highly connected nodes are the theorems humans actually care about — the compression IS the value judgment.
The structural claim is strong: mathematics is not a subject with compression as a tool. Mathematics is the compression. The definitions, lemmas, and theorems are the hierarchical naming scheme that makes exponential complexity fit in linear space. Take away the naming and you don't simplify mathematics — you destroy it, because the objects were never tractable without the names.