Monoids and Mathematical Compressibility

Monoids model mathematical compressibility by turning “proofs and definitions” into “strings and reusable substrings” , and then measuring how much reach you gain when you’re allowed to reuse those substrings as new generators.[‌:cite[1]{ln=4}‌], [‌:cite[1]{ln=5}‌], [‌:cite[2]{ln=4}‌] 1) The basic modeling move: proofs → words in a monoid Formal mathematics is represented as a directed hypergraph of all deduction steps, and a proof is a sub hypergraph that can be flattened into a linear sequence (a string) of primitive symbols.[‌:cite[1]{ln=1}‌], [‌:cite[1]{ln=4}‌] A finitely generated monoid is then used as a toy model for these strings, where word length is “size” , and naming a substring for reuse (a macro) is “compression.” [‌:cite[1]{ln=5}‌] 2) Macros are literally “new generators” (definitions/lemmas as named chunks) A macro set $M=\{g i\}$ is modeled as extra generators, where each macro generator is defined to equal some word over the primitive generators: $g i=w i$.[‌:cite[3]{ln=1}‌] You then work in the augmented generating set $G' = G \cup M$, meaning you’re allowed to write expressions using both primitives and macros.[‌:cite[3]{ln=2}‌] ==Practical translation: “introducing a definition/theorem name” is modeled as “adding a new symbol you can use instead of re spelling a longer expression.”==[‌:cite[2]{ln=4}‌], [‌:cite[1]{ln=5}‌] 3) Compression is measured via “expansion” (coverage) Instead of directly counting “how many tokens you save,” the paper measures the flip side : how much bigger a region you can cover with short expressions once macros exist.[‌:cite[4]{ln=2}‌], [‌:cite[4]{ln=3}‌] They define an expansion function : $f {G'}(s)=\sup\{r\in\mathbb{N}: B G(r)\subseteq B {G'}(s)\}$[‌:cite[5]{ln=3}‌] Here, $B G(r)=\{w: w G \le r\}$ is the ball of radius $r$ in the primitive length metric, and $B {G'}(s)$ is the same idea but measured using the enriched alphabet $G'$.[‌:cite[5]{ln=4}‌] So $f {G'}(s)$ says: using budget $s$ in the compressed language, what’s the largest primitive radius $r$ you can fully express.[‌:cite[5]{ln=6}‌] 4) Why different monoids imply different compressibility regimes They compare two extremes: the free abelian monoid $A n$ and free (non abelian) monoid $F n$.[‌:cite[1]{ln=7}‌], [‌:cite[6]{ln=10}‌] In $A n$, generators commute, so elements behave like vectors in $\mathbb{N}^n$ and balls grow polynomially .[‌:cite[1]{ln=8}‌], [‌:cite[7]{ln=3}‌] In $F n$, order matters and elements are strings, and balls grow exponentially .[‌:cite[6]{ln=12}‌], [‌:cite[7]{ln=5}‌] This growth rate difference drives how effective sparse macros can be: logarithmically many macros can give exponential expansion in $A n$, while even polynomially dense macros only give linear expansion in $F n$.[‌:cite[8]{ln=2}‌], [‌:cite[8]{ln=3}‌] 5) Connecting to “human math” vs “formal math” The authors argue human mathematics is “compressible through hierarchically nested concepts” (definitions/lemmas/theorems), and they model that compressibility with monoids and macros.[‌:cite[9]{ln=3}‌], [‌:cite[2]{ln=3}‌], [‌:cite[2]{ln=4}‌] They distinguish reductive compression (local substitution/expansion of definitions) from general algorithmic compression, and explicitly say this local, definitional notion is what they mean by “compression.”[‌:cite[10]{ln=1}‌], [‌:cite[10]{ln=4}‌] They then claim HM lives in the compressible regions of FM—where definitions actually provide leverage—because large parts of FM resist this kind of local compression.[‌:cite[11]{ln=4}‌], [‌:cite[12]{ln=6}‌] If you want the “coach takeaway”: ==think of monoids as a controlled playground where “definitions” are treated as explicit, countable resources (extra generators), and compressibility becomes a measurable tradeoff between how many definitions you store (macro density) and how much expressive power you gain (expansion).==[‌:cite[3]{ln=1}‌], [‌:cite[5]{ln=3}‌], [‌:cite[13]{ln=3}‌], [‌:cite[13]{ln=6}‌]