Paper deep dive
Compression is all you need: Modeling Mathematics
Vitaly Aksenov, Eve Bodnia, Michael H. Freedman, Michael Mulligan
Intelligence
Status: succeeded | Model: anthropic/claude-sonnet-4.6 | Prompt: intel-v1 | Confidence: 95%
Last extracted: 3/24/2026, 2:59:38 AM
Summary
This paper argues that human mathematics (HM) is distinguished from formal mathematics (FM) by its compressibility through hierarchically nested definitions, lemmas, and theorems. The authors model this using monoids: the free abelian monoid A_n and the free non-abelian monoid F_n. They prove that in A_n, logarithmically sparse macro sets achieve exponential expansion, while in F_n even polynomial-density macro sets yield only linear expansion. Empirical validation against MathLib (a large Lean 4 library) shows that unwrapped length grows exponentially with depth and wrapped length, consistent with A_n behavior. The paper proposes compression and PageRank-style analysis of the MathLib dependency graph as measures of mathematical interest to guide automated reasoning.
Entities (32)
Relation Signals (23)
Michael Mulligan → affiliatedwith → University of California, Riverside
confidence 99% · Department of Physics and Astronomy, University of California, Riverside, CA 92521, USA
Michael H. Freedman → affiliatedwith → Harvard University
confidence 99% · Center of Mathematical Sciences and Applications, Harvard University, Cambridge, MA 02138, USA
Michael Mulligan → affiliatedwith → Logical Intelligence
confidence 99% · Michael Mulligan, Logical Intelligence
Vitaly Aksenov → affiliatedwith → Logical Intelligence
confidence 99% · Vitaly Aksenov, Logical Intelligence aksenov@logicalintelligence.com
Eve Bodnia → affiliatedwith → Logical Intelligence
confidence 99% · Eve Bodnia, Logical Intelligence evebodnia@logicalintelligence.com
Michael H. Freedman → affiliatedwith → Logical Intelligence
confidence 99% · Michael H. Freedman, Logical Intelligence
Human Mathematics (HM) → issubsetof → Formal Mathematics (FM)
confidence 99% · Human mathematics (HM), the mathematics humans discover and value, is a vanishingly small subset of formal mathematics (FM)
MathLib → writtenin → Lean 4
confidence 99% · MathLib, a large repository of mathematics written in Lean 4
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Human mathematics (HM), the mathematics humans discover and value, is a vanishingly small subset of formal mathematics (FM), the totality of all valid deductions. We argue that HM is distinguished by its compressibility through hierarchically nested definitions, lemmas, and theorems. We model this with monoids. A mathematical deduction is a string of primitive symbols; a definition or theorem is a named substring or macro whose use compresses the string. In the free abelian monoid $A_n$, a logarithmically sparse macro set achieves exponential expansion of expressivity. In the free non-abelian monoid $F_n$, even a polynomially-dense macro set only yields linear expansion; superlinear expansion requires near-maximal density. We test these models against MathLib, a large Lean~4 library of mathematics that we take as a proxy for HM. Each element has a depth (layers of definitional nesting), a wrapped length (tokens in its definition), and an unwrapped length (primitive symbols after fully expanding all references). We find unwrapped length grows exponentially with both depth and wrapped length; wrapped length is approximately constant across all depths. These results are consistent with $A_n$ and inconsistent with $F_n$, supporting the thesis that HM occupies a polynomially-growing subset of the exponentially growing space FM. We discuss how compression, measured on the MathLib dependency graph, and a PageRank-style analysis of that graph can quantify mathematical interest and help direct automated reasoning toward the compressible regions where human mathematics lives.
Tags
Links
- Source: https://arxiv.org/abs/2603.20396v1
- Canonical: https://arxiv.org/abs/2603.20396v1
Trouble viewing inline? Open PDF directly →
Full Text
82,527 characters extracted from source content.
Expand or collapse full text
Compression is all you need: Modeling Mathematics Vitaly Aksenov Vitaly Aksenov, Logical Intelligence aksenov@logicalintelligence.com , Eve Bodnia Eve Bodnia, Logical Intelligence evebodnia@logicalintelligence.com , Michael H. Freedman Michael H. Freedman, Logical Intelligence; Center of Mathematical Sciences and Applications, Harvard University, Cambridge, MA 02138, USA michael.freedman@logicalintelligence.com, mfreedman@cmsa.fas.harvard.edu and Michael Mulligan Michael Mulligan, Logical Intelligence; Department of Physics and Astronomy, University of California, Riverside, CA 92521, USA michael.mulligan@logicalintelligence.com, michael.mulligan@ucr.edu Abstract. Human mathematics (HM), the mathematics humans discover and value, is a vanishingly small subset of formal mathematics (FM), the totality of all valid deductions. We argue that HM is distinguished by its compressibility through hierarchically nested definitions, lemmas, and theorems. We model this with monoids. A mathematical deduction is a string of primitive symbols; a definition or theorem is a named substring or macro whose use compresses the string. In the free abelian monoid AnA_n, a logarithmically sparse macro set achieves exponential expansion of expressivity. In the free non-abelian monoid FnF_n, even a polynomially-dense macro set only yields linear expansion; superlinear expansion requires near-maximal density. We test these models against MathLib, a large Lean 4 library of mathematics that we take as a proxy for HM. Each element has a depth (layers of definitional nesting), a wrapped length (tokens in its definition), and an unwrapped length (primitive symbols after fully expanding all references). We find unwrapped length grows exponentially with both depth and wrapped length; wrapped length is approximately constant across all depths. These results are consistent with AnA_n and inconsistent with FnF_n, supporting the thesis that HM occupies a polynomially-growing subset of the exponentially growing space FM. We discuss how compression, measured on the MathLib dependency graph, and a PageRank-style analysis of that graph can quantify mathematical interest and help direct automated reasoning toward the compressible regions where human mathematics lives. 1. Introduction In this paper, we argue that math is soft and squishy—that this is its defining characteristic. By “math” we do not mean the totality of all possible formal deductions, formal mathematics (FM), but rather human mathematics (HM), the type of arguments humans find and those we will appreciate when our AI agents find them for us.111However mathematics is formalized, we know from Gödel and other sources that there will be true statements without proofs (such as consistency of the system). It is possible that extremely simple Π10 ^0_1 statements of Peano arithmetic, such as the Goldbach conjecture (GC: “Every even number >2>2 is the sum of two primes”), could be both true and without any proof. Since our discussion is anchored to the concept of proof, we would not count GC as part of HM or even FM if that is the case, despite the fact that it is of interest to humans. A more subtle question: suppose GC has a proof but the shortest one is 1010010^100 lines long—is it part of HM? Fortunately we do not have to adjudicate this; our results are not sharp enough to require us to identify an exact frontier to HM. Moreover, HM might more precisely be considered a measure on FM that fades out rather than abruptly terminating at the edge of a subset; see [1]. By “soft and squishy,” we mean compressible through the use of hierarchically nested concepts: definitions, lemmas, and theorems. The finding that math is about compression is not new. We were scooped 3,000 years ago by the invention of place notation. Consider ℕN, the natural numbers, with generating set 1\1\. Place notation introduces additional symbols, or macros: “10” for ten ones, “100” for ten tens, and so on. With logarithmically many macros, expressivity expands exponentially. This (exponential) expansion of expressivity is the flip side of notational compression. Creating and exploiting definitions expands what we can reach by compressing expressions written in a primitive, definition-poor language. (Our theorems below will be stated in terms of expansion; our informal discussions often use compression.) Formal mathematics can be viewed as a directed hypergraph (DH) emerging from axioms and syntactical rules [1]. The DH records the full deduction space: every possible proof step, with each hyperedge specifying which premises are combined (Fig. 1, left). A proof is a sub-hypergraph of the DH; flattened into a linear sequence, it becomes a string of primitive symbols. We study finitely-generated monoids as models for such strings: word length measures size, and naming a substring for reuse—a macro—compresses it. (Monoids with relations can simulate Turing machines [13], so, despite its simplicity, this basic framework is computationally universal.) The simplest case is A1=ℕA_1=N, the natural numbers. To study compression more generally, we consider the free abelian monoid AnA_n and the free (non-abelian) monoid FnF_n (with n denoting the number of generators). In AnA_n, the generators commute, so only the multiplicities matter. In FnF_n, the order of generators is important, and there are no relations; since formal proofs are strings of symbols where order matters, FnF_n might be presumed to model formal deduction. We will argue, contrary this expectation, that the compression exhibited by human mathematics is characteristic of AnA_n, not FnF_n. Our main theoretical results quantify the expansion that macros achieve in AnA_n and FnF_n. In AnA_n, logarithmically many macros achieve exponential expansion (Theorem 1), and macros of polynomial density (growth exponent 1/k1/k) can yield infinite expansion—every element expressible with bounded length—via Waring’s theorem (Theorem 3). In FnF_n even polynomially growing macros (polynomial as a function of radius, i.e., polylogarithmic as a function of volume) yield only linear expansion (Theorem 4). Superlinear expansion in FnF_n requires an exponential number of macros (Theorem 5), in contrast with the logarithmically sparse macro set that suffices for exponential expansion in AnA_n. This difference reflects underlying growth rates: balls grow polynomially in AnA_n but exponentially in FnF_n. Our study of macro sets in AnA_n extends straightforwardly to the much larger class of free nilpotent monoids; they have nearly identical expansion properties to AnA_n and can equally serve as models for HM according to the analysis presented here (see Sections 4.3 for details). FM DHA∧B∧CA B CA∧BA BCCAAB∧CB CMathLib DAGA∧B∧CA B CA∧BA BCC Figure 1. A FM DH fragment (left) and a corresponding MathLib DAG (right) for deriving A∧B∧CA B C via ∧ -introduction. In the DH, filled dots represent hyperedges: each groups the premises used in a single inference step. Both proofs (via A∧BA B and via B∧CB C) are recorded. The DAG selects one proof and replaces the hyperedge with ordinary edges. If both proofs in the DH were recorded within a DAG, there would be an ambiguity in how a given conclusion followed from the premises. Note also that the above example is special in the sense that the hyperedges are reversible. We test these facts against MathLib [10], a large repository of mathematics written in Lean 4 [7] that contains hundreds of thousands of definitions, lemmas, and theorems. We use MathLib as a proxy for HM. MathLib can be viewed as a DAG extracted from the full deduction hypergraph (Fig. 1). Each MathLib element is a named subgraph of this DAG, rooted at the element itself and extending down to primitives. Flattening this subgraph by recursively expanding all references yields a string of primitives. The wrapped length counts the tokens in an element’s defining expression; the unwrapped length counts the primitives in the flattened string. We find the longest element, when fully unwrapped, reaches approximately 1010410^104 primitive terms—Googol, the number, not the company.222AlgebraicGeometry.Scheme.exists_hom_hom_comp_eq_comp_of_locallyOfFiniteType in MathLib; see Section 3 for discussion. Our primary observations about MathLib are as follows. First, unwrapped length grows exponentially with depth (the longest path to primitives in the dependency graph). Second, wrapped length is approximately constant across all depths. Third, unwrapped length grows exponentially with wrapped length. The MathLib data is consistent with the AnA_n logarithmic-density regime and inconsistent with the FnF_n alternatives we study. Our central inference is that HM is a thin subset of polynomial growth within the exponentially growing space FM. This is a stronger claim than the observation that HM is a vanishingly small subset of FM: the latter would hold if both grew exponentially at different rates [16, 6]. We propose AnA_n as a model for HM and products ∏FniΠ F_n_i as a model for FM. Since HM ⊂ FM, the models must respect this inclusion; AnA_n embeds into ∏FniΠ F_n_i by sending each generator to a distinct factor. Our toy models map HM to monoids. What we observe clearly in both source and target is compression and hierarchical depth: in the monoid, both are deduced from a postulated macro set; in MathLib, both can be measured. The comparison allows us to infer properties of a hypothetical “macro set” for HM. Physical models often gain power by defining abstractions not directly observed—the vector potential in electromagnetism, the Hilbert space in quantum mechanics. Similarly, our model may not be surjective: some abstractions in the monoid—notably the macro set itself—may have no direct counterpart on the HM side. We do not identify a precise “macro set” within MathLib (or HM more generally) that maps to the macro set in the monoid, but regard this as a deep open problem, tantamount to locating the owner’s manual for HM. Place notation demonstrates two features of mathematics that our models can capture. The first is hierarchy: the recursive fashion in which notation, ideas, definitions, and proofs are fitted together. The second is parsimony: we have limited storage for new concepts, so definitions must be chosen to strike a balance between marking out landmarks in an infinite structure and not overtaxing our capacity to remember them. HM works where compression is possible—it suits our minds and supports our inherent laziness, allowing large strides across the mathematical landscape with minimal effort. Logarithmic density, as in powers of 1010, lies near this parsimony boundary. The results of Section 2 explore the parsimony/expansion tradeoff systematically, showing how expansion rates depend on macro density across several regimes. The MathLib data of Section 3 confirms the hierarchical structure quantitatively: log(unwrapped length) (unwrapped length) grows linearly with depth, with slope close to 11 bit per level. If compression characterizes human mathematics, it can also serve as a measure of mathematical interest. An element whose terse statement conceals an enormous proof body exhibits high deductive compression; an element that compresses dramatically when definitions are applied sits in a region where the definitional hierarchy is useful. We call the latter reductive compression. Section 5 develops these ideas into quantitative interest measures and a PageRank-style refinement [5] that accounts for an element’s role in supporting other high-value mathematics. The goal is to give AI agents exploring formal mathematics a sense of direction: stay where compression is possible. Various LLMs collaborated with us on the proofs of the theorems in Section 2. The symbol below indicates that the theorem has been formally verified in Lean 4 by Aleph [9], a theorem-proving system developed by Logical Intelligence. The remainder of the paper is organized as follows. Section 2 develops the monoid models and proves the main expansion theorems. Section 3 presents the MathLib analysis. Section 4 further discusses the results and related ideas. Section 5 considers future work on automating mathematical interest and related open questions. Appendix A contains additional expansion theorems for AnA_n. 2. Monoid Models We study two basic monoids on n generators G=a1,…,anG=\a_1,…,a_n\: the free abelian monoid AnA_n and the free monoid FnF_n. In AnA_n, generators commute, so elements essentially live in ℕnN^n with componentwise addition. In FnF_n, order matters and there are no relations; elements are finite strings over G. For an element or word w in either monoid, write |w|G|w|_G for its length: the sum of coefficients for AnA_n, or the string length for FnF_n. A macro set M=giM=\g_i\ consists of additional generators, each defined by gi=wig_i=w_i for some word wiw_i written in terms of elements from G. The augmented generating set is G′=G∪MG =G∪ M, and |w|G′|w|_G denotes the minimum number of G′G -generators needed to represent w. Conceptually, while each gi∈Mg_i∈ M is an individual macro, the set M itself represents a compression strategy. 333In logic and computer science, “macro” often refers to the transformation rule (the strategy) itself. Here, we maintain the monoid-theoretic convention where the macro is the resulting element, and the set M constitutes the strategy. We quantify the effectiveness of such a strategy with the expansion function, fG′(s)=supr∈ℕ:BG(r)⊆BG′(s).f_G (s)= \r :B_G(r) B_G (s)\. Here, the ball of radius r is BG(r)=w:|w|G≤rB_G(r)=\w:|w|_G≤ r\, with BG′(s)B_G (s) defined analogously. Since G⊆G′G G , we have |w|G′≤|w|G|w|_G ≤|w|_G and thus BG(s)⊆BG′(s)B_G(s) B_G (s). The expansion function measures the largest G-radius fully covered by the G′G -ball of radius s. Our main results are summarized in Table 1. For concreteness, the table states the AnA_n results for A1=ℕA_1=N; they extend to general AnA_n by taking n copies of each macro (one per generator), with the same asymptotic expansion rates. In AnA_n, balls grow polynomially (|BG(r)|=(r+n)|B_G(r)|= r+nn), and sparse macros yield dramatic expansion—exponential or even infinite. The polylogarithmic row reflects an upper bound (Theorem 2); we do not establish a matching lower bound, so the true expansion for such macros may lie strictly between exponential and quasi-exponential. In FnF_n, balls grow exponentially (|BG(r)|=nr+1−1n−1|B_G(r)|= n^r+1-1n-1), and expansion is linear for a polynomial-dense macro set and superlinear for an exponentially-growing macro set. Monoid Macro M Density Expansion fG′(s)f_G (s) Theorem A1A_1 mk:m≥1\m^k:m≥ 1\ r1/kr^1/k ∞ 3 A1A_1 bjp:j≥1\b^j^p:j≥ 1\ (logr)1/p( r)^1/p ≤ec⋅slogs≤ e^c· s s 2 A1A_1 bj:j≥1\b^j:j≥ 1\ logr r Θ(bcs) (b^cs) 1 A1A_1 bbj:j≥0\b^b^j:j≥ 0\ logblogr _b r sb/(b−1)s^b/(b-1) to s(2b−1)/(b−1)s^(2b-1)/(b-1) 6 A1A_1 finite O(1)O(1) Θ(s) (s) 7 FnF_n polynomial rpr^p O(s)O(s) 4 FnF_n probabilistic nr/logrn^r/ r ≥ecs≥ e^c s 5 Table 1. Macro density versus expansion. For AnA_n with n>1n>1, expansion rates remain the same. The expansion properties for AnA_n also hold for free nilpotent monoids. The FnF_n polynomial result holds for any polynomial density and n≥2n≥ 2; up to constants, it holds for any finitely presented monoid of exponential growth. The FnF_n probabilistic result gives a macro set of logarithmically-vanishing density (|M∩Sr|/|Sr|∼1/log(r)→0|M∩ S_r|/|S_r| 1/ (r)→ 0), where Sr=w:|w|G=rS_r=\w:|w|_G=r\. We now proceed to the theorems that characterize expansion of different macro sets in AnA_n and FnF_n. The detailed proofs are not required for the later parts of the paper. 2.1. Free Abelian Monoid Place notation is the archetypal example of compression in AnA_n. Theorem 1 (Place notation gives exponential expansion ). For AnA_n and any integer b≥2b≥ 2, the macro set M=bjai:i=1,…,n,j≥1M=\b^ja_i:i=1,…,n,\ j≥ 1\ has logarithmic density and satisfies bs/(n(b−1))−1≤fG′(s)≤nb⋅bs/(n(b−1))b^s/(n(b-1))-1≤ f_G (s)≤ nb· b^s/(n(b-1)) for all integers s≥1s≥ 1. In particular, fG′(s)=Θ(bs/(n(b−1)))f_G (s)= (b^s/(n(b-1))). Proof. The macro set M=gi,j=bjai:i=1,…,n,j≥1M=\g_i,j=b^ja_i:i=1,…,n,\ j≥ 1\ has logarithmic density: the number of macros with |gi,j|G=bj≤r|g_i,j|_G=b^j≤ r is n⌊logbr⌋=O(logr)n _br =O( r). Lower bound. Any element w∈Anw∈ A_n can be written uniquely as w=x1a1+x2a2+⋯+xnanw=x_1a_1+x_2a_2+·s+x_na_n with xi∈ℕx_i . Writing each nonzero xix_i in base b as xi=∑j=0Jici,jbjx_i= _j=0^J_ic_i,jb^j with ci,j∈0,1,…,b−1c_i,j∈\0,1,…,b-1\ and Ji=⌊logbxi⌋J_i= _bx_i , we have xiai=ci,0ai+ci,1gi,1+ci,2gi,2+⋯+ci,Jigi,Ji.x_ia_i=c_i,0a_i+c_i,1g_i,1+c_i,2g_i,2+·s+c_i,J_ig_i,J_i. The G′G -length of xiaix_ia_i is ∑j=0Jici,j≤(b−1)(Ji+1)=(b−1)(⌊logbxi⌋+1) _j=0^J_ic_i,j≤(b-1)(J_i+1)=(b-1)( _bx_i +1). For w∈BG(r)w∈ B_G(r), we have |w|G=∑ixi≤r|w|_G= _ix_i≤ r, so each xi≤rx_i≤ r and thus |w|G′≤∑i=1n(b−1)(⌊logbxi⌋+1)≤n(b−1)(logbr+1).|w|_G ≤ _i=1^n(b-1)( _bx_i +1)≤ n(b-1)( _br+1). Therefore BG(r)⊆BG′(s)B_G(r) B_G (s) whenever s≥n(b−1)(logbr+1)s≥ n(b-1)( _br+1), which gives fG′(s)≥bs/(n(b−1))−1f_G (s)≥ b^s/(n(b-1))-1. Upper bound. We exhibit a hard-to-compress element. For any integer k≥1k≥ 1, define wk=(bk−1)(a1+⋯+an)w_k=(b^k-1)(a_1+·s+a_n). Then |wk|G=n(bk−1)|w_k|_G=n(b^k-1). Since bk−1=∑j=0k−1(b−1)bjb^k-1= _j=0^k-1(b-1)b^j, |wk|G′=n(b−1)k|w_k|_G =n(b-1)k. Now given s≥1s≥ 1, choose k=⌊s/(n(b−1))⌋+1k= s/(n(b-1)) +1. Then |wk|G′=n(b−1)k>s|w_k|_G =n(b-1)k>s, so wk∉BG′(s)w_k∉ B_G (s). Since wk∈BG(n(bk−1))⊆BG(nbk)w_k∈ B_G(n(b^k-1)) B_G(nb^k), we have BG(nbk)⊈BG′(s)B_G(nb^k) B_G (s), and thus fG′(s)<nbk≤nb⋅bs/(n(b−1)).f_G (s)<nb^k≤ nb· b^s/(n(b-1)). Combining the bounds gives fG′(s)=Θ(bs/(n(b−1)))f_G (s)= (b^s/(n(b-1))). ∎ We next establish an upper bound: with polylogarithmically many macros, expansion is at most quasi-exponential. Theorem 2 (Polylogarithmic density gives quasi-exponential expansion ). For AnA_n, let M⊆AnM A_n be a macro set with polylogarithmic growth: |M∩BG(r)|≤c(log(e+r))qfor all r≥0,|M∩ B_G(r)|≤ c( (e+r))^q all r≥ 0, for some constants c,q>0c,q>0. Then there exists a constant K>0K>0 depending only on n,c,qn,c,q such that fG′(s)≤exp(Kslogs)for all s≥2.f_G (s)≤ (Ks s) all s≥ 2. Proof. Fix s∈ℕs and suppose BG(r)⊆BG′(s)B_G(r) B_G (s), i.e., every element of length ≤r≤ r can be expressed as a sum of at most s generators from G′=G∪MG =G∪ M. We derive an upper bound on r in terms of s. Step 1: Only macros of length ≤r≤ r are relevant. Let w∈BG(r)w∈ B_G(r) and write w=y1+⋯+ykw=y_1+·s+y_k with k≤sk≤ s and yi∈G′y_i∈ G . Each yiy_i has length |yi|G≥0|y_i|_G≥ 0, and additivity of length in ℕnN^n gives |w|G=|y1|G+⋯+|yk|G|w|_G=|y_1|_G+·s+|y_k|_G. Since |w|G≤r|w|_G≤ r, all |yi|G≤r|y_i|_G≤ r; otherwise their sum would exceed r. Thus, in any representation of elements of BG(r)B_G(r), only generators of length ≤r≤ r can appear. Define Mr:=M∩BG(r)M_r:=M∩ B_G(r), so that |Mr|≤c(log(e+r))q|M_r|≤ c( (e+r))^q, and note that in every such representation each yiy_i lies in G∪MrG∪ M_r. Let t(r):=|G∪Mr|=n+|Mr|≤(n+c)(log(e+r))q.t(r):=|G∪ M_r|=n+|M_r|≤(n+c)( (e+r))^q. Step 2: Upper bound on the number of words of length ≤s≤ s. The number of words of length ≤s≤ s over an alphabet of size t(r)t(r) is at most Nwords(r,s):=∑k=0st(r)k≤(s+1)(n+c)s(log(e+r))qs.N_words(r,s):= _k=0^st(r)^k≤(s+1)(n+c)^s( (e+r))^qs. Each such word represents some element of AnA_n. By our assumption BG(r)⊆BG′(s)B_G(r) B_G (s) and Step 1, every element of BG(r)B_G(r) is representable by at least one such word. Thus |BG(r)|≤Nwords(r,s)|B_G(r)|≤ N_words(r,s). Since |BG(r)|=(r+n)≥rnn!|B_G(r)|= r+nn≥ r^nn!, we have rnn!≤(s+1)(n+c)s(log(e+r))qs. r^nn!≤(s+1)(n+c)^s( (e+r))^qs. Taking logarithms, for sufficiently large s: (1) nlogr≤(1+log(n+c))s+qsloglog(e+r).n r≤(1+ (n+c))s+qs (e+r). Step 3: Bounding r. We show that (1) fails for K>2q/nK>2q/n and sufficiently large s whenever logr≥Kslogs r≥ Ks s. It suffices to consider logr=Kslogs r=Ks s, since larger r only further violates the inequality. For large s: loglog(e+r)≤log2+log(Kslogs)≤log(2K)+2logs. (e+r)≤ 2+ (Ks s)≤ (2K)+2 s. Substituting into (1) gives: nKslogs≤(1+log(n+c)+qlog(2K))s+2qslogs.nKs s≤(1+ (n+c)+q (2K))s+2qs s. Dividing by slogs s: nK≤1+log(n+c)+qlog(2K)logs+2q.nK≤ 1+ (n+c)+q (2K) s+2q. For large s, the right-hand side approaches 2q2q, so choosing K>2q/nK>2q/n yields a contradiction. Thus fG′(s)<exp(Kslogs)f_G (s)< (Ks s) for all sufficiently large s. For small s, the bound in Step 2 shows fG′(s)f_G (s) is finite (since the polynomial growth in r eventually beats the polylog growth in r), so by enlarging K if necessary, the bound fG′(s)≤exp(Kslogs)f_G (s)≤ (Ks s) holds for all s≥2s≥ 2. ∎ Finally, we show that polynomial-density macros can yield infinite expansion. Theorem 3 (Polynomial density gives infinite expansion ). For any integer k≥2k≥ 2, there exists a macro set M⊆AnM A_n such that: |M∩BG(r)|≤nr1/kfor all r≥1,|M∩ B_G(r)|≤ nr^1/k all r≥ 1, and fG′(s)=∞for all s≥ng(k),f_G (s)=∞ all s≥ ng(k), where g(k)g(k) is the Waring constant (the smallest integer such that every nonnegative integer is a sum of at most g(k)g(k) k-th powers). Proof. For each generator ai∈Ga_i∈ G and each m∈ℕm , define the macro gi,m:=mkaig_i,m:=m^ka_i. Let M:=mkai:i=1,…,n,m≥1.M:=\m^ka_i:i=1,…,n,\ m≥ 1\. Growth bound. A macro mkaim^ka_i has G-length mkm^k. The number of macros with |gi,m|G=mk≤r|g_i,m|_G=m^k≤ r is ⌊r1/k⌋ r^1/k for each i, so |M∩BG(r)|=n⌊r1/k⌋≤nr1/k.|M∩ B_G(r)|=n r^1/k ≤ nr^1/k. Infinite expansion. Any element w∈Anw∈ A_n can be written as w=x1a1+⋯+xnanw=x_1a_1+·s+x_na_n with xi∈ℕx_i . By Waring’s theorem, each xix_i is a sum of at most g(k)g(k) k-th powers: xi=mi,1k+⋯+mi,tik,ti≤g(k).x_i=m_i,1^k+·s+m_i,t_i^k, t_i≤ g(k). Thus xiai=mi,1kai+⋯+mi,tikai,x_ia_i=m_i,1^ka_i+·s+m_i,t_i^ka_i, where each term mi,jkaim_i,j^ka_i lies in M. Summing over all i, the total number of macro terms is at most ∑i=1nti≤ng(k) _i=1^nt_i≤ ng(k). Hence every element of AnA_n lies in BG′(ng(k))B_G (ng(k)), giving fG′(ng(k))=∞f_G (ng(k))=∞. ∎ Remark 1. For k=2k=2, Lagrange’s four-square theorem gives g(2)=4g(2)=4, so a macro set of squares with growth exponent 1/21/2 achieves fG′(4)=∞f_G (4)=∞. Remark 2. The macro sets in Theorems 1 and 3 exhibit a sort of duality: Theorem 1 uses powers of a fixed base bjai:j≥1\b^ja_i:j≥ 1\, while Theorem 3 uses fixed powers of varying bases mkai:m≥1\m^ka_i:m≥ 1\. The sparser logarithmic-density set achieves exponential expansion; the polynomial-density set achieves infinite expansion. Additional results for AnA_n, including the cases of double-logarithmic and finite macro density, appear in Appendix A. 2.2. Free Monoid In contrast to AnA_n, we now show that for FnF_n, a polynomially-growing macro set only achieves linear expansion and that superlinear expansion requires an exponentially-growing macro set. This reflects the exponential growth of the underlying monoid. Theorem 4 (Polynomial density gives linear expansion ). For FnF_n with n≥2n≥ 2, let M be a macro set with at most cℓpc ^p macros of each G-length ℓ≥2 ≥ 2, for some constants c>0c>0 and p≥0p≥ 0. Then there exists a constant d=d(n,p,c)d=d(n,p,c) such that for all integers s≥1s≥ 1: fG′(s)<ds.f_G (s)<ds. Moreover, it suffices to choose an integer d≥3d≥ 3 satisfying: (2) nd>4e(n+c)dp+1.n^d>4e(n+c)d^p+1. Proof. Fix integers r,s≥1r,s≥ 1. Consider words of exact G-length r: Sr:=w∈Fn:|w|G=r,|Sr|=nr.S_r:=\w∈ F_n:|w|_G=r\, |S_r|=n^r. We will show that for an appropriate choice of d, |w∈Sds:|w|G′≤s|<nds|\w∈ S_ds:|w|_G ≤ s\|<n^ds, which implies BG(ds)⊈BG′(s)B_G(ds) B_G (s). Fix r=dsr=ds and 1≤k≤s1≤ k≤ s. Since FnF_n has no relations, any representation w=y1⋯ykw=y_1·s y_k with yi∈G′y_i∈ G and |w|G=ds|w|_G=ds is determined by: (1) A composition of dsds into k positive parts (ℓ1,…,ℓk)( _1,…, _k), where ℓi=|yi|G _i=|y_i|_G (2) A choice of generator in G′G of G-length ℓi _i for each i For each length ℓ≥1 ≥ 1, there are at most (n+c)ℓp(n+c) ^p generators in G′G of that length (exactly n for ℓ=1 =1, at most cℓpc ^p for ℓ>1 >1). Therefore: |(y1,…,yk):yi∈G′,|yi|G=ℓi|≤(n+c)k∏i=1kℓip≤(n+c)k(dsk)pk,|\(y_1,…,y_k):y_i∈ G ,|y_i|_G= _i\|≤(n+c)^k _i=1^k _i^p≤(n+c)^k ( dsk )^pk, where the right-most inequality follows from AM-GM with ∑i=1kℓi=ds _i=1^k _i=ds: ∏i=1kℓi≤(dsk)k. _i=1^k _i≤ ( dsk )^k. There are (ds−1k−1) ds-1k-1 such compositions, so: |w∈Sds:|w|G′=k|≤(ds−1k−1)(n+c)k(dsk)pk.|\w∈ S_ds:|w|_G =k\|≤ ds-1k-1(n+c)^k ( dsk )^pk. Summing over k≤sk≤ s: |w∈Sds:|w|G′≤s|≤∑k=1s(ds−1k−1)(n+c)k(dsk)pk≤(ds−1s−1)∑k=1s(n+c)k(dsk)pk.|\w∈ S_ds:|w|_G ≤ s\|≤ _k=1^s ds-1k-1(n+c)^k ( dsk )^pk≤ ds-1s-1 _k=1^s(n+c)^k ( dsk )^pk. The second inequality uses the fact that for d≥2d≥ 2 and 1≤k≤s1≤ k≤ s, we have (ds−1k−1)≤(ds−1s−1) ds-1k-1≤ ds-1s-1. Define: Σs:=∑k=1s(n+c)k(dsk)pk. _s:= _k=1^s(n+c)^k ( dsk )^pk. Writing bk:=((n+c)dp(sk)p)kb_k:= ((n+c)d^p ( sk )^p )^k, one can verify that if (n+c)dp≥ep(n+c)d^p≥ e^p, the sequence bkb_k is increasing in k for 1≤k≤s1≤ k≤ s. Since d≥3d≥ 3 and n+c≥2n+c≥ 2, we have (n+c)dp≥2⋅3p>ep(n+c)d^p≥ 2· 3^p>e^p, so the monotonicity condition holds. Thus Σs≤s⋅bs=s⋅((n+c)dp)s≤(2(n+c)dp)s _s≤ s· b_s=s·((n+c)d^p)^s≤(2(n+c)d^p)^s. Using (ds−1s−1)<(ds)≤(ed)s ds-1s-1< dss≤(ed)^s: |w∈Sds:|w|G′≤s|≤(ed)s(2(n+c)dp)s=(2e(n+c)dp+1)s.|\w∈ S_ds:|w|_G ≤ s\|≤(ed)^s(2(n+c)d^p)^s=(2e(n+c)d^p+1)^s. Choose d such that nd>4e(n+c)dp+1n^d>4e(n+c)d^p+1. Then |w∈Sds:|w|G′≤s|≤(2e(n+c)dp+1)s<(nd/2)s<nds.|\w∈ S_ds:|w|_G ≤ s\|≤(2e(n+c)d^p+1)^s<(n^d/2)^s<n^ds. Therefore not all words of G-length dsds lie in BG′(s)B_G (s), so fG′(s)<dsf_G (s)<ds. ∎ Remark 3. When p=0p=0, condition (2) simplifies to nd>4e(n+c)dn^d>4e(n+c)d, recovering the logarithmic-density case. The next result shows that a macro set of vanishing sphere density—though still exponentially large in absolute terms—allows for superlinear expansion. Theorem 5 (Probabilistic sparse macros give superlinear expansion in FnF_n ). Let FnF_n be the free monoid on n≥2n≥ 2 generators G=a1,…,anG=\a_1,…,a_n\. There exists a macro set M⊂FnM⊂ F_n such that |M∩Sr||Sr|⟶0as r→∞, |M∩ S_r||S_r| 0 r→∞, and fG′(s)s⟶∞as s→∞, f_G (s)s ∞ s→∞, where Sr=w∈Fn:|w|G=rS_r=\w∈ F_n:|w|_G=r\, G′=G∪MG =G∪ M, and fG′f_G is the expansion function. More quantitatively, there exist constants K,c>0K,c>0 (depending only on n) such that BG(r)⊆BG′(K(logr)2)for all sufficiently large r,B_G(r) B_G \! (K( r)^2 ) all sufficiently large r, and hence fG′(s)≥exp(cs)for all sufficiently large s.f_G (s)\ ≥\ \! (c s ) all sufficiently large s. Proof. We build M as a union of a small deterministic family of log-periodic words and an independent random family. Step 0: log-periodic words. For a word w=b1⋯bL∈Fnw=b_1·s b_L∈ F_n of length L=|w|GL=|w|_G, say that w has period d if 1≤d≤L1≤ d≤ L and bj=bj+db_j=b_j+d for all 1≤j≤L−d1≤ j≤ L-d. Write per(w)per(w) for the least such d. Fix constants C>4lognC>4 n and B≥2CB≥ 2C (natural logarithms). Define the deterministic macro family P:=w∈Fn:per(w)≤Blog(e+|w|G).P\,:=\, \w∈ F_n:\ per(w)≤ B (e+|w|_G ) \. Step 1: random macros of density 1/logℓ1/ . Independently for each word u∈Fnu∈ F_n of length ℓ≥2 ≥ 2, include u in a random set R with probability pℓ:=1log(e+ℓ).p_ \ :=\ 1 (e+ ). Let M:=P∪RM:=P∪ R and G′:=G∪MG :=G∪ M. Step 2: vanishing sphere density. We have |Sr|=nr|S_r|=n^r. First, count the deterministic part: any word in P∩SrP∩ S_r is determined by its period d≤Blog(e+r)d≤ B (e+r) and its first d letters, hence |P∩Sr|≤∑d≤Blog(e+r)nd≤nBlog(e+r)+1=O(rBlogn).|P∩ S_r|\ ≤\ _d≤ B (e+r)n^d\ ≤\ n^B (e+r)+1\ =\ O (r^B n ). So |P∩Sr|/nr→0|P∩ S_r|/n^r→ 0. Second, |R∩Sr||R∩ S_r| is Bin(nr,pr)Bin(n^r,p_r) with mean μr=nr/log(e+r) _r=n^r/ (e+r). A Chernoff bound gives Pr(|R∩Sr|≥2μr)≤exp(−μr/3), (|R∩ S_r|≥ 2 _r )\ ≤\ (- _r/3), and ∑rexp(−μr/3)<∞ _r (- _r/3)<∞ since μr _r grows exponentially. By Borel–Cantelli, almost surely |R∩Sr|≤2nr/log(e+r)|R∩ S_r|≤ 2n^r/ (e+r) for all large r. Thus, almost surely, |M∩Sr||Sr|≤|P∩Sr|nr+|R∩Sr|nr≤o(1)+2log(e+r)⟶ 0. |M∩ S_r||S_r|\ ≤\ |P∩ S_r|n^r+ |R∩ S_r|n^r\ ≤\ o(1)+ 2 (e+r)\ \ 0. Step 3: a halving lemma (one macro consumes half the word). Fix a length r and set k(r):=⌈Clog(e+r)⌉.k(r)\ :=\ C (e+r) . For a word w=b1⋯br∈Srw=b_1·s b_r∈ S_r, consider the family of long early substrings r(w):=bibi+1⋯bi+ℓ−1: 1≤i≤k(r),⌈r/2⌉≤ℓ≤r−i+1.C_r(w)\ :=\ \\,b_ib_i+1·s b_i+ -1\ :\ 1≤ i≤ k(r),\ r/2 ≤ ≤ r-i+1\, \. Each element of r(w)C_r(w) has length between ⌈r/2⌉ r/2 and r. Claim. For every w∈Srw∈ S_r, either r(w)C_r(w) contains an element of P, or else all words in r(w)C_r(w) are pairwise distinct. Indeed, if two elements of r(w)C_r(w) were equal, they must have the same length ℓ . So we would have bi⋯bi+ℓ−1=bj⋯bj+ℓ−1for some 1≤i<j≤k(r).b_i·s b_i+ -1\,=\,b_j·s b_j+ -1 some 1≤ i<j≤ k(r). Let d=j−i≤k(r)d=j-i≤ k(r). Then the word u=bi⋯bi+ℓ+d−1u=b_i·s b_i+ +d-1 has period d, hence per(u)≤d≤k(r)≤Clog(e+r)≤Blog(e+|u|G),per(u)≤ d≤ k(r)≤ C (e+r)≤ B (e+|u|_G ), for r large (since |u|G≍r|u|_G r and B≥2CB≥ 2C). Thus u∈Pu∈ P, and in particular r(w)C_r(w) contains an element of P. This proves the claim. Now suppose r(w)∩P=∅C_r(w)∩ P= . Then the claim says r(w)C_r(w) is a set of distinct words. Also, a crude count gives |r(w)|≥k(r)(⌊r/2⌋−k(r))≥r4k(r)|C_r(w)|\ ≥\ k(r) ( r/2 -k(r) )\ ≥\ r4\,k(r) for all large r (since k(r)=O(logr)k(r)=O( r)). Because each u∈r(w)u _r(w) has length ≥r/2≥ r/2, we have p|u|G≥1/log(e+r)p_|u|_G≥ 1/ (e+r). Independence of the random choice of R across distinct words gives Pr(r(w)∩R=∅)=∏u∈r(w)(1−p|u|G)≤exp(−∑u∈r(w)p|u|G)≤exp(−|r(w)|log(e+r)). (C_r(w)∩ R= )\ =\ _u _r(w)(1-p_|u|_G)\ ≤\ \! (- _u _r(w)p_|u|_G )\ ≤\ \! (- |C_r(w)| (e+r) ). Using |r(w)|≥r4k(r)|C_r(w)|≥ r4k(r) and k(r)=⌈Clog(e+r)⌉k(r)= C (e+r) gives Pr(r(w)∩R=∅)≤exp(−C4r). (C_r(w)∩ R= )\ ≤\ \! (- C4r ). Therefore, for every w∈Srw∈ S_r, Pr(r(w)∩M=∅)≤exp(−C4r), (C_r(w)∩ M= )\ ≤\ \! (- C4r ), since if r(w)C_r(w) meets P then it certainly meets M. By a union bound over all w∈Srw∈ S_r, Pr(∃w∈Sr with r(w)∩M=∅)≤nrexp(−C4r)=exp(r(logn−C/4)). (∃\,w∈ S_r with C_r(w)∩ M= )\ ≤\ n^r \! (- C4r )\ =\ (r( n-C/4) ). Since C>4lognC>4 n, the right-hand side is summable in r. By Borel–Cantelli, with probability 11 there is r0r_0 such that for all r≥r0r≥ r_0 every word w∈Srw∈ S_r satisfies r(w)∩M≠∅C_r(w)∩ M≠ . Equivalently: for all large r, every length-r word has a macro (deterministic or random) of length ≥r/2≥ r/2 starting within its first k(r)k(r) letters. Step 4: recursive parsing and the (logr)2( r)^2 bound. Fix r≥r0r≥ r_0 and a word w∈Srw∈ S_r. From Step 3, choose 1≤i≤k(r)1≤ i≤ k(r) and ℓ≥r/2 ≥ r/2 such that u:=bi⋯bi+ℓ−1∈M.u:=b_i·s b_i+ -1∈ M. Then we can write w=(b1⋯bi−1)⋅u⋅(bi+ℓ⋯br),w\,=\,(b_1·s b_i-1)\ ·\ u\ ·\ (b_i+ ·s b_r), where the prefix (b1⋯bi−1)(b_1·s b_i-1) uses i−1≤k(r)i-1≤ k(r) generators from G (fillers), and u is one macro. The suffix has length at most r−ℓ≤r/2r- ≤ r/2. Apply the same procedure to the suffix, and iterate. After at most ⌈log2r⌉ _2r iterations the remaining suffix has bounded length and can be spelled out with generators. At each iteration, we spend at most k(r)+1=O(logr)k(r)+1=O( r) tokens (fillers plus one macro). Thus there is a constant K such that every w∈Srw∈ S_r has |w|G′≤K(logr)2|w|_G \ ≤\ K( r)^2 for all r large. Since |w|G′|w|_G is monotone in |w|G|w|_G, the same bound holds for every word of length ≤r≤ r, i.e. BG(r)⊆BG′(K(logr)2)for all large r.B_G(r) B_G \! (K( r)^2 ) all large r. This gives the claimed expansion bound. Writing s=K(logr)2s=K( r)^2 implies r=exp(s/K)r= ( s/K), so fG′(s)≥exp(cs)f_G (s)≥ (c s) with c=1/Kc=1/ K. In particular fG′(s)/s→∞f_G (s)/s→∞. ∎ Remark 4. The macro set M exists almost surely under the random inclusion process, but no explicit construction is given. Remark 5. The sphere density of M satisfies |M∩Sr|/|Sr|∼2/logr|M∩ S_r|/|S_r| 2/ r. In absolute terms, |M∩Sr|∼2nr/logr|M∩ S_r| 2n^r/ r: a vanishing fraction of each sphere, but exponentially many macros at each radius. This contrasts with Theorem 4, where at most cℓpc ^p macros per length forces linear expansion. 3. Interpreting Data from MathLib We now compare the results of Section 2 against MathLib. We will think of MathLib as a proxy for HM. Of course, MathLib’s structure is partly shaped by Lean’s type theory and by the choices of its contributor community. Because MathLib is still small (roughly 500,000 elements in the version used in this study444Commit d167c6dc962ab340507362ea2f4bcfcff44f01b, dated 17 October 2025.) and unevenly developed, we see prominent finite-size effects at its frontier. This limits our ability to infer precise dimensional properties, but the data is consistent with low-dimensional behavior more characteristic of AnA_n than FnF_n. 3.1. Constructing the dependency graph We construct a dependency graph from MathLib’s internal Lean representation. The vertices are all MathLib elements: lemmas, theorems, definitions, structures, and inductive types, plus a synthetic node for types (Sort) and Lean core library elements (And, Nat, List, etc.) that have no further MathLib dependencies. Each MathLib element has two parts: a signature (the theorem statement or type definition) and an optional body (the proof or defining expression). For each element u, we count how many times each other element v is referenced, producing a directed edge from u to v weighted by this count. Edges thus point toward dependencies. The resulting data for each element is a vector of reference counts. Note that this construction only records the multiplicity of each reference and forgets the order in which references appear within an element’s expression tree. For example, two proofs that apply the same lemmas with the same multiplicities but in different ways produce identical dependency graph entries. As a simple example, consider: ⬇ 1lemma simple_lemma A B : Prop : A /\ B -> B := 2 fun h : A /\ B => And.right h For reference, its internal representation is: ⬇ 1type: forallE (A : Sort 0), forallE (B : Sort 0), 2 forallE (_ : app (app And #1) #0), #1 3body: lam (A : Sort 0) => lam (B : Sort 0) => 4 lam (h : app (app And #1) #0) => app (app (app And.right #2) #1) #0 The signature contains two occurrences of Sort (for the Prop type of A and B) and one of And. The body contains Sort twice, And once, and And.right once. These produce weighted edges from simple_lemma to the corresponding elements. To extract these dependencies, we recursively traverse each MathLib element’s signature and body, collecting every const node (representing a reference to a named declaration): ⬇ 1def collectElems (e : Expr) (acc : HashMap Name Nat := ): HashMap Name Nat := 2 match e with 3 | .const declName _ => acc.insert declName (acc.getD declName 0 + 1) 4 | .app fn arg => collectElems arg (collectElems fn acc) 5 | .lam _ binderType body _ => collectElems body (collectElems binderType acc) 6 | .forallE _ binderType body _ => collectElems body (collectElems binderType acc) 7 | .letE _ type value body _ => collectElems body (collectElems value (collectElems type acc)) 8 | .mdata _ expr => collectElems expr acc 9 | .proj _ _ struct => collectElems struct acc 10 | .sort _ => acc.insert (Name.mkSimple "Sort") (acc.getD (Name.mkSimple "Sort") 0 + 1) 11 | _ => acc The key case is .const declName _, which represents a reference to a named declaration; each such occurrence produces an edge in our graph. The other cases (app for function application, lam for lambda abstraction, forallE for dependent arrows, letE for let-bindings) simply recurse into their subexpressions. We also count .sort occurrences, treating Sort (which, for example, represents Prop) as a primitive. The resulting graph contains a small number of cycles (approximately 60 pairs of mutually dependent elements, all involving unsafe recursion). Since our analysis requires an acyclic graph, we collapse each strongly connected component into a single vertex, reducing the vertex count from 463,719 to 463,661. 3.2. Wrapped and unwrapped lengths, and depth Lean core library elements and Sort (primitive elements) form the sinks of the MathLib DAG and are analogous to the generators G in our monoid models. We consider all other (non-primitive) elements to be analogous to the macro set M. Thus, we view MathLib as G′=G∪MG =G∪ M. The unwrapped length of an element u, denoted by |u|G|u|_G, is the total count of primitives when all references are recursively expanded. Primitives have unwrapped length 11. For any non-primitive element with edges to elements v1,…,vkv_1,…,v_k with weights w1,…,wkw_1,…,w_k: |u|G=∑i=1kwi⋅|vi|G.|u|_G= _i=1^kw_i·|v_i|_G. As the notation indicates, unwrapped length corresponds directly to the G-length in the monoid model. The wrapped length of an element u is its token length: the number of tokens in its definition written in Lean as produced by the Lean parser. Wrapped length corresponds to |u|G′∖u|u|_G \u\ in the monoid model. One could alternatively define wrapped length as the number of references in the internal Lean representation, i.e., the total weight of outgoing edges in the dependency graph. However, tactics such as simp and rw expand during elaboration into many internal references to basic elements, inflating the reference count of some elements without introducing deep dependencies. Under the reference-count metric, this produces elements with large wrapped length but slowly growing unwrapped length—a plateau in the compression curve that reflects proof automation rather than mathematical content. Token count avoids this artifact: a tactic invocation is a single token regardless of how many references it generates internally. Some MathLib elements are generated internally by Lean and have no human-written source; we omit these when reporting wrapped lengths. The depth of an element is the length of the longest path to primitives in the dependency DAG, i.e., the maximum number of successive reference-expansion steps required to reach generators. Primitives have depth 0. 3.3. Distributions of wrapped and unwrapped lengths, and depth Figures 2(a)–(c) show the distributions of elements by log2(unwrapped length) _2(unwrapped length), wrapped length, and depth. In each case, the distribution is concentrated at low values with a long tail. The declines at large values reflect finite-size effects: MathLib’s coverage is uneven, and we expect the tails to extend and fill in as the library grows. A future analysis tracking MathLib’s evolution over time could measure how the frontier expands. (a) (b) (c) Figure 2. Distributions of MathLib elements by (a) log2(unwrapped length) _2(unwrapped length), (b) wrapped length, and (c) depth. 3.4. Unwrapped length versus wrapped length Figure 3 shows median log2(unwrapped length) _2(unwrapped length) versus wrapped length. While fG′(s)f_G (s) measures the coverage of G′G , these data points reflect the realized G-lengths |u|G|u|_G achieved by MathLib’s compression strategy. The approximately linear relationship between log2(unwrapped length) _2(unwrapped length) and wrapped length (slope ≈0.4≈ 0.4 bits/token) indicates exponential expansion: each additional token yields a roughly constant multiplicative gain in primitive count. Further interpretation is provided in Section 3.7. Notice the spike at small wrapped length. This arises from the following types of elements, but not restricted to them: (1) abbreviations, such as isOpenMap_proj from the module Topology.VectorBundle.Basic with wrapped length 77 and unwrapped length 104810^48; (2) “final” theorems using complex intermediate ones, such as integrable from the module Analysis.Calculus.BumpFunction.Normed with wrapped length 99 and unwrapped length 2⋅10542· 10^54; (3) special cases of complex statements, such as infinitesimal_zero from the module Analysis.Real.Hyperreal with wrapped length 88 and unwrapped length 3.6⋅10313.6· 10^31. (Hyperlinks are located under the module name.) Figure 3. Median log2(unwrapped length) _2(unwrapped length) versus wrapped length. Each point represents the median over all elements at that wrapped length. 3.5. Wrapped length versus depth Figure 4 shows the median wrapped length as a function of depth. The relationship is approximately flat (with at most a mild positive slope): (ignoring outliers at large depth) median wrapped length hovers in the range of roughly 50–120 across depths 0–300, with no strong dependence on depth. This means that individual definitions do not become systematically longer as depth increases, reminiscent of the powers of 10 macro of place notation. This is not surprising since defining expressions are unlikely to become arbitrarily long; instead we expect modularization as wrapped length increases. Figure 4. Median wrapped length versus depth. 3.6. Unwrapped length versus depth Figure 5 shows the median log2(unwrapped length) _2(unwrapped length) as a function of depth. The relationship is approximately linear with slope close to 1, indicating that unwrapped length grows exponentially with depth: each additional layer of definitions provides a roughly constant multiplicative gain in primitive count. The maximum depth reaches approximately 300, consistent with the maximum unwrapped length of approximately 1010410^104, achieved by the algebraic geometry entry noted in the introduction. Figure 5. Median log2(unwrapped length) _2(unwrapped length) versus depth. The approximately linear relationship indicates exponential growth of unwrapped length with depth. 3.7. Discriminating between regimes To make contact between the MathLib measurements and the monoid models of Section 2, we need to establish a correspondence between unwrapped length, wrapped length, depth, and their analogs in the monoid. Unwrapped length corresponds directly to the G-length |u|G|u|_G in the monoid: both count the total number of primitive symbols after fully expanding all references. The wrapped length of an element u∈G′u∈ G in the monoid is |u|G′∖u|u|_G \u\: the minimum cost to represent u using all generators in G′=G∪MG =G∪ M except u itself, where each generator (primitive or macro) contributes cost 11. This mirrors the MathLib convention, where the wrapped length of an element is its token count—the cost of writing the definition using all available named elements. The depth of an element u in the monoid generated by G′G is defined recursively using optimal representations.555For general monoids this definition will not be algorithmically computable due to lack of or limited cancellation; the definition is effective for AnA_n, NilnNil_n (discussed later), and FnF_n. Every primitive g∈Gg∈ G has depth 0. For any element u with u∉Gu∉ G, compute the optimal representation of u in G′∖uG \u\; if this uses only primitives then depth(u)=1depth(u)=1, and otherwise depth(u)=1+maxdepth(v):v∈M∖u,v appears in the optimal representation of u.depth(u)=1+ \,\depth(v):v∈ M \u\,\ v appears in the optimal representation of u\. Depth thus measures the length of the longest chain of macro dependencies required to optimally express u, bottoming out at primitives. (Note that the expansion theorems of Section 2 impose only density conditions on the macro set.) This is analogous, but not identical to MathLib depth, which uses the longest path to primitives in the dependency DAG: MathLib depth reflects authorial choices, while monoid depth reflects the intrinsic hierarchical structure under optimal compression. We note that we measured these quantities on all named elements in MathLib, not on all possible expressions that could be formed from them. Accordingly, in each monoid regime we restrict to the elements of the generating set G′=G∪MG =G∪ M, rather than to all elements of the ambient monoid. Table 2 summarizes the relationships among the three quantities for each monoid regime. The Parsimony column indicates whether the macro set grows at a strictly slower rate than the ambient monoid: subpolynomial macro growth in AnA_n, or subexponential macro growth in FnF_n. Parsimonious macro sets achieve exponential expansion in AnA_n but only linear expansion in FnF_n. We discuss each row in turn below, specializing to A1=ℕA_1=N and F2F_2 whenever no generality is lost. Regime log|w|G |w|_G vs depth |w|G′∖w|w|_G \w\ vs depth log|w|G |w|_G vs |w|G′∖w|w|_G \w\ Parsimony AnA_n, log density Linear Flat∗ Degenerate∗ Yes AnA_n, Waring Linear Flat Degenerate No AnA_n, double-log Exponential Doubly exp. Logarithmic Yes FnF_n, polynomial Degenerate Degenerate Logarithmic Yes FnF_n, probabilistic Linear Quadratic Concave (⋅ ·) No Table 2. Predicted relationships among log|w|G |w|_G (log unwrapped length), |w|G′∖w|w|_G \w\ (wrapped length), and depth for each monoid regime. Measurements are restricted to elements of G′=G∪MG =G∪ M. “Degenerate” means the independent variable (i.e., the “x” in “y vs x”) is bounded. The asterisk (∗ ) indicates that if a generic element of the monoid is considered then Flat → Linear and Degenerate → Linear; see 3.7.6 for discussion. 3.7.1. AnA_n, logarithmic-density macros (Theorem 1) The macro set is M=bjai:i=1,…,n,j≥1M=\b^ja_i:i=1,…,n,\ j≥ 1\. We specialize to A1A_1 with M=bj:j≥1M=\b^j:j≥ 1\. Macro bjb^j has G-length bjb^j, so log|bj|G=jlogb |b^j|_G=j b. Its optimal representation in G′∖bjG \b^j\ uses b copies of bj−1b^j-1, giving wrapped length b, independent of j. Iterating this, depth(bj)=jdepth(b^j)=j. Thus, log|w|G |w|_G is linear in depth, wrapped length is flat across all depths, and since wrapped length is constant while log|w|G |w|_G varies freely, the third relationship is degenerate. If one considers generic elements of A1A_1 rather than restricting to macro elements, the picture changes for columns 2 and 3. A generic element x∈ℕx has a wrapped length ∼logx x and depth ∼logx x. Thus wrapped length generally grows linearly with depth, and log|x|G∼|x|G′∖x |x|_G |x|_G \x. 3.7.2. AnA_n, polynomial-density macros / Waring (Theorem 3) The macro set is M=mk:m≥1M=\m^k:m≥ 1\ for fixed k≥2k≥ 2 (specializing to A1A_1). Macro mkm^k has G-length mkm^k, so log|mk|G=klogm |m^k|_G=k m. By Waring’s theorem, mkm^k can be written as a sum of at most g(k)g(k) k-th powers of strictly smaller integers, so wrapped length is at most g(k)g(k), independent of m. We don’t know the optimal decomposition at each stage, but can bound the depth: a halving strategy (expressing mkm^k using k-th powers of integers ≈m/2≈ m/2, then recursing) gives depth O(logm)O( m) and a linear relationship in column 1; slower reductions give greater depth and a sublinear relationship, down to logarithmic if depth ∼m m. In all cases, wrapped length remains bounded, so columns 2 and 3 are flat and degenerate respectively. The Waring and log-density regimes produce identical predictions in the first three columns of Table 2 but differ in parsimony. In contrast to the log-density case, for generic elements of A1A_1 in the Waring regime, column 3 remains degenerate since every x∈ℕx has wrapped length at most g(k)g(k). 3.7.3. AnA_n, double-logarithmic density (Theorem 6) The macro set is M=bbj:j≥0M=\b^b^j:j≥ 0\ (specializing to A1A_1). Macro mj=bbjm_j=b^b^j has log|mj|G=bjlogb |m_j|_G=b^j b, which grows exponentially in j=depth(mj)j=depth(m_j). The optimal representation of mjm_j in G′∖mjG \m_j\ uses ⌊mj/mj−1⌋=bbj−1(b−1) m_j/m_j-1 =b^b^j-1(b-1) copies of mj−1m_j-1, so wrapped length ∼bbj−1(b−1) b^b^j-1(b-1), which grows doubly exponentially in depth. Eliminating j: log(wrapped)∼bj−1(b−1)logb∼b−1blog|mj|G (wrapped) b^j-1(b-1) b b-1b |m_j|_G, so log|mj|G∼b−1log(wrapped) |m_j|_G bb-1 (wrapped), giving a logarithmic relationship in column 3. The first three columns are inconsistent with the MathLib data. 3.7.4. FnF_n, polynomial-density macros (Theorem 4) The macro set has at most cℓpc ^p elements of each G-length ℓ , out of nℓn total words of that length in FnF_n. The fraction of words at length ℓ that are macros is therefore cℓp/nℓc ^p/n , which vanishes exponentially fast. For any macro m with |m|G=r|m|_G=r, the probability that its optimal representation in G′∖mG \m\ contains another macro is negligible: the exponentially sparse macro set cannot populate the exponentially growing spheres of FnF_n densely enough to sustain hierarchical nesting. Consequently, essentially all macros have depth 11, with their optimal representations consisting almost entirely of primitives. Thus, log|m|G |m|_G vs depth and wrapped vs depth are degenerate. Since log|m|G≈log(wrapped) |m|_G≈ (wrapped), the column 3 entry is logarithmic. Again, the first three column entries are inconsistent with MathLib. 3.7.5. FnF_n, probabilistic sparse macros (Theorem 5) Here the macro set has ∼2nr/logr 2n^r/ r elements at radius r: exponentially many, though a logarithmically vanishing fraction (|M∩Sr|/|Sr|∼2/logr|M∩ S_r|/|S_r| 2/ r) of the sphere. This contrasts with the polynomial case, where the fraction vanishes exponentially. The absolute density is sufficient for the halving scheme of Theorem 5 to work: (nearly) every word of length r has a macro of length ≥r/2≥ r/2 starting within its first k(r)=O(logr)k(r)=O( r) positions. Hierarchical depth develops as a result. For a macro m with |m|G=r|m|_G=r, the halving scheme gives depth(m)∼log2rdepth(m) _2r, so log|m|G∼depth |m|_G . For the wrapped length: at each of the ∼log2r _2r levels, we spend at most k(rt)=O(logrt)k(r_t)=O( r_t) primitive fillers plus one macro, where rt≤r/2tr_t≤ r/2^t is the remaining length at level t. The total wrapped length is wrapped≤∑t=0log2rO(log(r/2t))=∑t=0log2rO(logr−t)=O((logr)2),wrapped≤ _t=0 _2rO( (r/2^t))= _t=0 _2rO( r-t)=O(( r)^2), where the sum is arithmetic with O(logr)O( r) terms each of size O(logr)O( r). Since depth∼logrdepth r, wrapped =O(depth2)=O(depth^2). Eliminating depth: log|m|G∼depth∼wrapped |m|_G wrapped, giving a concave (⋅ ·) relationship in column 3. 3.7.6. Summary and Identifying the “Macro Set” The MathLib data (Figures 3, 4, and 5) shows: an approximately linear relationship in column 1, an approximately flat relationship in column 2, and an approximately linear relationship in column 3. The FnF_n regimes are inconsistent with the data in at least two of the three columns. The AnA_n log-density and Waring regimes both match columns 1 and 2 for macro elements, but predict a degenerate column 3. For generic elements in the log-density regime (recall the asterisks in Table 2), columns 2 and 3 both become linear. The MathLib column 2 plot is approximately flat but may have a mild positive slope, consistent with a mixture of macro and generic elements in the log-density regime. This points to AnA_n with log-density macros, which we note is also the parsimonious regime. We do not take the all-non-primitives identification seriously as the true “macro set” for MathLib. MathLib contains abbreviations and trivial specializations (see Section 3.4) that merely invoke deep elements, contributing little compression on their own. On the other hand, some elements contribute substantial compression, e.g., the filter abstraction that unifies many limit theorems into a single framework. The identification of the correct “macro set” is a central problem. One simple approach to refining the “macro set” is to filter by in-degree in the dependency graph, removing elements in the bottom x percentile for varying x. Removing an element from M leaves unwrapped lengths unchanged, but increases wrapped lengths and decreases depths. Another option is to restrict the “macro set” to definition-like elements, e.g., those whose resulting type is Sort; we found that the resulting macro set provides little compression. One could also formulate the problem as an optimization, e.g., given a dependency DAG, find the “macro set” of fixed size k that minimizes the total wrapped length. Whether these or related approaches bring the three metrics into better agreement with the AnA_n log-density predictions is an open question. The difficulty of identifying the “macro set” may reflect limitations of MathLib itself as a proxy for HM. An enriched representation that captures relationships MathLib leaves implicit (e.g., that a family of related theorems are instances of a single pattern), or permits (as a hypergraph does) storage of multiple proofs of the same theorem, might admit a more satisfactory “macro set.” Finding a representation with an identifiable “macro set” is not merely a question of library science: it could reveal new mathematical structure and help direct automated agents. 4. Discussion 4.1. Why monoids? Monoids model the sequential structure of proofs; for the dependency structure, where multiple premises are consumed simultaneously, n-categories and “globular magmas” offer alternative frameworks. Inspired by the “growth of groups” [11], which is essentially independent of generating set, one might expect that the choice of formal system should not greatly affect the shape of mathematics. However, the recursive nature of mathematics leads to unexpectedly large distortions: rewriting between different formulations of a mathematical theory with identical proof power can be non-recursively inefficient (see [1] and references therein). If rules and syntax are fixed, the underlying minimal-proof DAG is a discrete metric space with the axioms as base point. This metric geometry is modeled by the Cayley-graph geometry of each monoid and underlies the concepts of polynomial and exponential growth. 4.2. Why monoids rather than groups Groups introduce inverses, and inverses complicate the expansion analysis. This difficulty has historical precedent: Post [13] encoded the halting problem into the word problem for monoids in 1947, but extending this to groups required another decade of work by Boone and Novikov [12, 4]. The gap reflects the technical complications that inverses introduce. For our purposes, the problem is concrete. In the free group, any word w can be written with length 2 by choosing macros m and m′m that nearly cancel: mm′=wmm =w. By making m and m′m sufficiently long, we can do this for every word while keeping the macro density arbitrarily small. This “cancellation trick” trivializes the expansion question for groups. One might object that deduction rules like Modus Ponens (A→BA→ B, A⊢BA B) involve a kind of cancellation. However, reversible logic is universal with only modest overhead [2], so cancellation is not essential to computation. More pragmatically, free monoids admit exact analysis—we stand where the light is good. While on the topic of groups, there is a Lie-theoretic analogy worth noting: the inclusion An↪∏i=1nFniA_n _i=1^nF_n_i resembles the inclusion of a maximal torus Tn−1↪SO(n)T^n-1 SO(n). If AnA_n is broadened to free-nilpotent monoids Niln,kNil_n,k (n counting homological rank and k the nilpotency level), then the inclusion Niln,k↪∏i=1nFniNil_n,k _i=1^nF_n_i is reminiscent of the Iwasawa decomposition G=KANG=KAN of a semisimple Lie group. 4.3. Nilpotent and solvable monoids The dichotomy between AnA_n and FnF_n reflects different growth rates: polynomial versus exponential. This difference, not abelian versus non-abelian, is what matters. The nonnegative Heisenberg monoid illustrates the polynomial-growth case.666The nonnegative Heisenberg monoid consists of 3×33× 3 nonnegative integer matrices with zeros below the diagonal and ones on the diagonal. It can be presented as ⟨a,b,z∣ab=baz,az=za,bz=zb⟩ a,b,z ab=baz,az=za,bz=zb . It is nilpotent and non-abelian, and of polynomial growth. Here again, and in all free nilpotent monoids, logarithmic-density macros yield exponential expansion, just as for AnA_n. The proof is simple. Niln,kNil_n,k is the monoid with n “base” generators, with additional secondary generators to simulate commutation, and the minimal relations needed to encode the level-k right-nested commutators (recall we have no inverses in these monoids). All these generators, and their number is polynomial in n and k, individually generate a copy of ℕN. Build separate macro sets in each of these ℕN-directions. Then take the union of these ℕN-macro-sets to be the macro set for Niln,kNil_n,k. Up to polynomial factors it will have the same expansion function as the mini-macro-sets in each ℕN. Among monoids with cancellation (meaning ac=bcac=bc implies a=ba=b, and ca=cbca=cb implies a=ba=b), the geometrically crucial property of “polynomial growth” is characterized (as in groups) by Gromov’s criterion [8]: they are sub-monoids of finite index within a nilpotent monoid. So there is at hand a well-understood class of slow-growth monoids to help us model HM. The nonnegative sector of the SOL lattice illustrates the exponential-growth case. This monoid is solvable and non-abelian—more structured than a free monoid—but still has exponential growth. Counting arguments parallel to Theorem 4 show that it admits no poly-logarithmically growing macro with super-linear expansion. 4.4. Why formal mathematics resists compression That human mathematics compresses well is familiar from experience and confirmed by our MathLib analysis. Less obvious is that FM, as a whole, must contain vast regions that resist compression. By compression we mean something specific: reductive compression, the local substitution of definitions, not arbitrary algorithmic encoding. The digits of π illustrate the distinction. The number π has low Kolmogorov complexity—a short program computes it—but the digit string admits no known local compression via pattern substitution. Reductive compression requires finding a repeated structure to name. High reductive compressibility does, however, imply low Kolmogorov complexity, since the DAG of definitions encodes a short reconstruction procedure. Moreover, this procedure runs in at most linear time, so reductively compressible elements have low logical depth in the sense of Bennett [3]. Thus reductive compressibility is a more restrictive condition than low Kolmogorov complexity. With this understanding, the incompressibility of most of FM follows from standard complexity assumptions. Consider theorems of the form “the Boolean formula S is unsatisfiable.” We argue that for typical S such theorems lie outside HM. Such statements are easy to write down, but for generic S the shortest proofs are believed to be exponentially long—essentially, one must check all possible variable assignments. No system of definitions can shortcut this exhaustive search. If such proofs could be radically compressed, this would contradict the assumption P≠NP≠ NP. Thus HM consists of the compressible regions of FM—the mathematics where definitions provide leverage. This motivates our search for monoid models that are highly compressible (modeling HM) yet embed in larger monoids that resist compression (modeling FM). Compressibility may even serve as a first approximation to mathematical taste; Section 5 develops this idea, distinguishing reductive compression (shortening statements via definitions) from deductive compression (shortening proofs given statements) and using PageRank to combine both into an automated measure of mathematical interest. 4.5. Comparison with cellular automata Kolmogorov complexity anticipates the action of any possible algorithm and thus has no locality restriction, whereas reductive compression requires the algorithm to act locally. A cellular automaton (CA) also acts locally, but on a fixed lattice or graph. In reductive compression, the underlying lattice also undergoes collapsing at each step (as well as changing its site labels); this kind of dynamic may be called a “collapsing cellular automaton” (CCA), and is how we think of compression operationally. 4.6. A self-referential remark In writing this paper, we have introduced a new mathematical concept: the expansion function fG′(s)f_G (s). This generalizes a notion from additive number theory. The additive rank of a subset S⊆ℕS is the fewest copies of S whose sumset equals ℕN; the asymptotic rank is the fewest copies whose sumset is cofinal in ℕN. When S is too sparse for any finite number of copies to cover ℕN, these notions break down. Our expansion function measures instead how large a ball can be covered by sums of at most s elements from G′G —a natural generalization when infinite coverage is impossible. That we were led to introduce a definition while studying the role of definitions in mathematics is perhaps fitting. Definition formation is so natural to mathematical practice that even analyzing math requires new definitions. 5. Application and Outlook Can we give AI agents a sense of direction—an automated criterion for which mathematical statements merit attention? Surely historical and cultural factors influence human judgments of mathematical interest, but here we attempt to identify observables intrinsic to the mathematical representations themselves (see also [1]). G G′∖uG \u\ S |S|G|S|_G |S|G′∖u|S|_G \u\ B |B|G|B|_G |B|G′∖u|B|_G \u\ Table 3. Four measures of an element with signature S (statement) and body B (proof). The ratio across rows measures reductive compression; the ratio down the G′∖uG \u\ column measures deductive compression. The central thesis of this paper suggests compressibility as a natural candidate. Here we consider two types. For any element u in a mathematical corpus, whether a definition, lemma, or theorem, define the reductive compression: T0(u)=|S|G+|B|G|S|G′∖u+|B|G′∖u,T_0(u)= |S|_G+|B|_G|S|_G \u\+|B|_G \u\, the ratio of unwrapped to wrapped length for the full element (signature plus body). Here, we are using the monoid notation defined in Section 3.7, where |⋅|G|·|_G corresponds to unwrapped length and |⋅|G′∖u|·|_G \u\ to wrapped length. Table 3 summarizes the four resulting measures of an element. Elements with large T0T_0 (“taste”) live in regions where definitions provide substantial leverage—precisely the regions we have identified with human mathematics. An agent exploring mathematics can track the average value of T0T_0 as it explores from region to region. This might assist it in staying close to HM. Although this risks biasing the agent toward abstraction—which should not be pursued for its own sake—T0T_0 can contribute to an agent’s sense of direction. The ratio of wrapped body length to wrapped signature length measures another type of compressibility, deductive compression777An alternative is |B|G/|S|G|B|_G/|S|_G, i.e., measured in G rather than G′∖uG \u\, which measures the primitive proof-to-statement ratio before compression. This would strongly reward theorems with naive statements (like Fermat’s Last Theorem) that require elaborate additional developments (the theory of elliptic curves) for their proof.: I0(u)=|B|G′∖u|S|G′∖u.I_0(u)= |B|_G \u\|S|_G \u\. Elements without bodies (primitives, structure declarations, inductive types) have I0=0I_0=0; they may still achieve high T0T_0 using definitions. Elements with large I0I_0 (“interest”) have short statements but long proofs, even after compression. In MathLib, elements with high I0I_0 include the deep theorems of algebraic geometry and category theory, where layers of abstraction compress enormous unwrapped expressions into manageable statements. One imagines that formalized versions of landmark results—Fermat’s Last Theorem, the Poincaré conjecture, resolution of singularities—would achieve exceptional compression ratios, their terse statements belying vast proof machinery. When statements become long enough to encode logical conundra, I0I_0 can be gamed: metamathematical constructions produce arbitrarily large values for elements of questionable interest. For example (and with thanks to Sam Buss), the theorem asserting k-consistency: that a formal system has no proof of 0=10=1 in fewer than k symbols, can have tiny compressed length, since recursive function theory allows the rapid description of certain enormously large integers k. However Pudlák [14, 15] showed that any proof of k-consistency in a sufficiently rich (and consistent) system must have length Ω(k1/2) (k^1/2)—no system of definitions can shortcut it. By taking k=B(n)k=B(n), B denoting the Busy Beaver function, one obtains a family of theorems with phenomenally large I0≈B1/2(k)/logkI_0 ^1/2(k)/ k that few would consider that interesting, at least on an individual basis, since this is merely one of a huge family, parameterized by k, of similar theorems; individually, they are logical curiosities rather than core mathematics. 5.1. A PageRank-style refinement The issue is that I0I_0 treats all high-compression elements equally, regardless of their role in the broader mathematical structure. A refinement should incorporate not just the compression achieved by an element, but also its usefulness in building other high-value elements. Google’s PageRank algorithm [5] offers a natural framework. Consider the full dependency graph, with edges pointing from each element to its dependencies. A random walk on this graph would accumulate at primitives—the sinks of the DAG—which achieve low compression and are not mathematically interesting in the sense we seek. The standard fix is teleportation: at each step, with probability α the walker follows an edge, and with probability 1−α1-α it jumps to a random node. Even with uniform teleportation, this may produce nontrivial rankings by identifying useful elements from graph structure alone. We suggest biasing teleportation toward high-compression elements. We parametrically combine our two compression measures into J0=βT0+(1−β)I0J_0=β T_0+(1-β)I_0 (after normalizing each to comparable scales) for some 0<β<10<β<1, and let an element u be chosen as the teleportation destination with probability J0(u)/∑vJ0(v)J_0(u)/ _vJ_0(v). The resulting transition matrix is P(v,u)=α⋅w(u,v)W(u)+(1−α)⋅J0(v)Z,P(v,u)=α· w(u,v)W(u)+(1-α)· J_0(v)Z, where w(u,v)w(u,v) is the number of times u references v, W(u)=∑xw(u,x)W(u)= _xw(u,x) is the total reference count of u, and Z=∑xJ0(x)Z= _xJ_0(x). A stationary distribution π satisfies ∑uP(v,u)π(u)=π(v) _uP(v,u)π(u)=π(v); standard PageRank theory (i.e., the Perron–Frobenius theorem) guarantees existence and uniqueness since every node has positive teleportation probability. Define I1(u)=π(u).I_1(u)=π(u). Elements score highly if they are either high-compression themselves (frequent teleportation destinations) or depended upon by elements that are visited often. This captures “load-bearing” elements: those that support the compressible regions of mathematics. We expect that α will need to be properly tuned to avoid trivial π, such as when all mass is concentrated at either the axioms or the largest J0J_0 elements in the DAG. 5.2. Some Open Questions First, the computational challenge: determining optimal compression requires searching over possible definitions, which is computationally expensive. Our interest measures assume a fixed set of definitions, but an agent exploring FM would need to propose new definitions on the fly. Can this be done efficiently enough to guide exploration? Second, definitional compression occupies one extreme of a spectrum. At the other extreme is Kolmogorov complexity, which allows arbitrary algorithmic compression but is uncomputable. Definitional compression is local and efficiently verifiable: applying a definition requires only checking that certain properties have been derived, and the process runs in at most linear time (in Bennett’s [3] terminology, it has low “logical depth”). Is there useful middle ground—compression methods more powerful than local substitution but still computationally tractable? Finally, we note an empirical question for MathLib and similar repositories: Do the proofs of “interesting” statements stay close to the ground (using only shallow intermediate lemmas), or do they take flight through highly compressed intermediate statements? In physical terms, what potential barriers must be overcome to reach deep theorems? The depth and mass distributions in Section 3 offer preliminary data, but a systematic study correlating these metrics with human judgments of interest remains to be done. References [1] M. Barkeshli, M. R. Douglas, and M. H. Freedman Artificial intelligence and the structure of mathematics. Note: To appear Cited by: §1, §4.1, §5, footnote 1. [2] C. H. Bennett (1973) Logical reversibility of computation. IBM Journal of Research and Development 17 (6), p. 525–532. Cited by: §4.2. [3] C. H. Bennett (1988) Logical depth and physical complexity. The Universal Turing Machine: A Half-Century Survey, p. 227–257. Cited by: §4.4, §5.2. [4] W. W. Boone (1959) The word problem. Annals of Mathematics 70 (2), p. 207–265. Cited by: §4.2. [5] S. Brin and L. Page (1998) The anatomy of a large-scale hypertextual web search engine. Computer networks and ISDN systems 30 (1-7), p. 107–117. Cited by: §1, §5.1. [6] T. M. Cover and J. A. Thomas (2006) Elements of information theory. 2nd edition, Wiley-Interscience. Note: See Chapter 3 for the Asymptotic Equipartition Property and the size of the Typical Set. External Links: ISBN 978-0-471-24195-9 Cited by: §1. [7] L. de Moura and S. Ullrich (2021) The Lean 4 theorem prover and programming language. In Automated Deduction – CADE 28, Lecture Notes in Computer Science, Vol. 12699, p. 625–635. Cited by: §1. [8] M. Gromov (1981) Groups of polynomial growth and expanding maps. Publications Mathématiques de l’IHÉS 53, p. 53–78. Cited by: §4.3. [9] Logical Intelligence (2025) Aleph. Note: https://logicalintelligence.com/ Cited by: §1. [10] Mathlib Community (2020) The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), New York, NY, USA, p. 367–381. External Links: Document Cited by: §1. [11] J. Milnor (1968) A note on curvature and fundamental group. Journal of Differential Geometry 2 (1), p. 1–7. External Links: Document Cited by: §4.1. [12] P. S. Novikov (1955) On the algorithmic unsolvability of the word problem in group theory. Trudy Matematicheskogo Instituta imeni V.A. Steklova 44, p. 1–143. Cited by: §4.2. [13] E. L. Post (1947) Recursive unsolvability of a problem of Thue. The Journal of Symbolic Logic 12 (1), p. 1–11. Cited by: §1, §4.2. [14] P. Pudlák (1986) On the length of proofs of finitistic consistency statements in first order theories. In Logic Colloquium ’84, p. 165–196. Cited by: §5. [15] P. Pudlák (1987) Improved bounds to the length of proofs of finitistic consistency statements. In Logic and Combinatorics, Contemporary Mathematics, Vol. 65, p. 309–331. Cited by: §5. [16] C. E. Shannon (1948) A mathematical theory of communication. Bell System Technical Journal 27 (3), p. 379–423. Note: The foundational text for the definition of entropy rate and redundancy in discrete sources. Cited by: §1. Appendix A Additional Expansion Theorems The following results complete the picture for A1=ℕA_1=N summarized in Table 1. Theorem 6 (Double-logarithmic density gives polynomial expansion ). For A1=ℕA_1=N and any integer b≥2b≥ 2, the macro set M=bbj:j≥0M=\b^b^j:j≥ 0\ has double-logarithmic density and satisfies c1sb/(b−1)≤fG′(s)≤c2s(2b−1)/(b−1)c_1\,s^b/(b-1)≤ f_G (s)≤ c_2\,s^(2b-1)/(b-1) for all s≥1s≥ 1, where c1,c2>0c_1,c_2>0 depend only on b. Proof. Let mj=bbjm_j=b^b^j for j≥0j≥ 0. The number of macros with G-length at most r is the number of j with bbj≤rb^b^j≤ r, i.e., j≤logblogbrj≤ _b _br. Thus M has double-logarithmic density. Greedy representation of mk−1m_k-1. The largest macro not exceeding mk−1m_k-1 is mk−1m_k-1. The number of copies used is ⌊mk−1mk−1⌋=⌊bbk−1(b−1)−b−bk−1⌋=bbk−1(b−1)−1, m_k-1m_k-1 = b^b^k-1(b-1)-b^-b^k-1 =b^b^k-1(b-1)-1, with remainder mk−1−1m_k-1-1. Letting Tk=|mk−1|G′T_k=|m_k-1|_G , we obtain Tk=(bbk−1(b−1)−1)+Tk−1,T0=b−1.T_k=(b^b^k-1(b-1)-1)+T_k-1, T_0=b-1. The first term dominates: Tk∼bbk−1(b−1)T_k b^b^k-1(b-1). The elements mk−1m_k-1 are hardest to compress. Let Sj=max|x|G′:x<mjS_j= \|x|_G :x<m_j\. We claim Sj=TjS_j=T_j for all j≥0j≥ 0. The base case S0=T0=b−1S_0=T_0=b-1 is clear. For the inductive step, suppose Sj=TjS_j=T_j and consider any x with mj≤x<mj+1m_j≤ x<m_j+1. Writing x=cj⋅mj+rx=c_j· m_j+r with 0≤r<mj0≤ r<m_j, we have |x|G′≤cj+Tj|x|_G ≤ c_j+T_j. Since cj≤bbj(b−1)−1c_j≤ b^b^j(b-1)-1, we obtain Sj+1≤Tj+1S_j+1≤ T_j+1. Equality holds at x=mj+1−1x=m_j+1-1. Upper bound. Fix s≥b−1s≥ b-1 and let k satisfy Tk≤s<Tk+1T_k≤ s<T_k+1. The element (s−Tk+1)mk+(mk−1)(s-T_k+1)m_k+(m_k-1) has G′G -length equal to (s−Tk+1)+Tk=s+1(s-T_k+1)+T_k=s+1, so it is not in BG′(s)B_G (s). Thus fG′(s)<(s+2)mkf_G (s)<(s+2)m_k. From the recurrence, Tk≥bbk−1(b−1)−1T_k≥ b^b^k-1(b-1)-1, so Tk≤sT_k≤ s implies bbk−1(b−1)≤s+1≤2sb^b^k-1(b-1)≤ s+1≤ 2s. Thus, bk−1≤logb(2s)b−1b^k-1≤ _b(2s)b-1 and we have mk=b⋅bk−1≤(2s)b/(b−1)m_k=b^b· b^k-1≤(2s)^b/(b-1). Therefore fG′(s)≤c2s(2b−1)/(b−1)f_G (s)≤ c_2\,s^(2b-1)/(b-1). For s<b−1s<b-1, we simply choose c2c_2 sufficiently large. Lower bound. With k as above, any x=c⋅mk+yx=c· m_k+y with 0≤y<mk0≤ y<m_k satisfies |x|G′≤c+Tk|x|_G ≤ c+T_k. If c≤s−Tkc≤ s-T_k then x∈BG′(s)x∈ B_G (s), so fG′(s)≥(s−Tk+1)mk−1f_G (s)≥(s-T_k+1)m_k-1. Case s≤2Tks≤ 2T_k. Then Tk≥s/2T_k≥ s/2, so mk=bbk≥cTkb/(b−1)≥c(s/2)b/(b−1)≥c1sb/(b−1)m_k=b^b^k≥ c\,T_k^b/(b-1)≥ c\,(s/2)^b/(b-1)≥ c_1\,s^b/(b-1). Since s−Tk+1≥1s-T_k+1≥ 1, we obtain fG′(s)≥csb/(b−1)f_G (s)≥ c\,s^b/(b-1). Case s>2Tks>2T_k. Then s−Tk+1≥s/2s-T_k+1≥ s/2. From s<Tk+1≤Cbbk(b−1)s<T_k+1≤ Cb^b^k(b-1) we obtain bk≥logb(s/C)b−1b^k≥ _b(s/C)b-1 and thus mk=bbk≥(s/C)1/(b−1)m_k=b^b^k≥(s/C)^1/(b-1). Therefore fG′(s)≥(s/2)(s/C)1/(b−1)≥c1sb/(b−1)f_G (s)≥(s/2)(s/C)^1/(b-1)≥ c_1\,s^b/(b-1). ∎ Theorem 7 (Finite macro gives linear expansion ). For A1=ℕA_1=N, let M be a finite macro set. Then fG′(s)=Θ(s)f_G (s)= (s). Proof. Let L=max|m|G:m∈ML= \|m|_G:m∈ M\ be the largest G-length among all macros. Upper bound. Any element x with |x|G′≤s|x|_G ≤ s is a sum of at most s generators from G′=G∪MG =G∪ M. Each generator has G-length at most L, so |x|G≤sL|x|_G≤ sL. Thus BG′(s)⊆BG(sL)B_G (s) B_G(sL), which gives fG′(s)≤sLf_G (s)≤ sL. Lower bound. Since G⊆G′G G , we have |x|G′≤|x|G|x|_G ≤|x|_G for all x. Thus BG(s)⊆BG′(s)B_G(s) B_G (s), which gives fG′(s)≥sf_G (s)≥ s. Combining the bounds gives fG′(s)=Θ(s)f_G (s)= (s). ∎ Remark 6. Theorems 6 and 7 extend to AnA_n with the macro sets bbjai:i=1,…,n,j≥0\b^b^ja_i:i=1,…,n,j≥ 0\ and any finite M⊆AnM A_n respectively, yielding the same asymptotic expansion rates.