Compression is all you need: Modeling Mathematics

Vitaly Aksenov; Eve Bodnia; Michael H. Freedman; Michael Mulligan

cs.AIMar 20, 2026

Compression is all you need: Modeling Mathematics

Authors: Vitaly Aksenov, Eve Bodnia, Michael H. Freedman, Michael Mulligan

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.

Figures & tables

Panel of Figure 1 — Figure 1. A FM DH fragment (left) and a corresponding MathLib DAG (right) for deriving $A\wedge B\wedge C$ via $\wedge$ -introduction. In the DH, filled dots represent hyperedges: each groups the premises used in a single inference step. Both proofs (via $A\wedge B$ and via $B\wedge 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.

Monoid	Macro $M$	Density	Expansion $f_{G^{\prime}}(s)$	Theorem
$A_{1}$	$\{m^{k}:m\geq 1\}$	$r^{1/k}$	$\infty$	3
$A_{1}$	$\{b^{j^{p}}:j\geq 1\}$	$(\log r)^{1/p}$	$\leq e^{c\cdot s\log s}$	2
$A_{1}$	$\{b^{j}:j\geq 1\}$	$\log r$	$\Theta(b^{cs})$	1
$A_{1}$	$\{b^{b^{j}}:j\geq 0\}$	$\log_{b}\log r$	$s^{b/(b-1)}$ to $s^{(2b-1)/(b-1)}$	6
$A_{1}$	finite	$O(1)$	$\Theta(s)$	7
$F_{n}$	polynomial	$r^{p}$	$O(s)$	4

Table 1. Macro density versus expansion. For

A_{n}

with

n>1

, expansion rates remain the same. The expansion properties for

A_{n}

also hold for free nilpotent monoids. The

F_{n}

polynomial result holds for any polynomial density and

n\geq 2

; up to constants, it holds for any finitely presented monoid of exponential growth. The

F_{n}

probabilistic result gives a macro set of logarithmically-vanishing density (

|M\cap S_{r}|/|S_{r}|\sim 1/\log(r)\to 0

), where

S_{r}=\{w:|w|_{G}=r\}

Panel of Figure 2 — Figure 2. Distributions of MathLib elements by (a) $\log_{2}(\text{unwrapped length})$ , (b) wrapped length, and (c) depth.

Figure 3. Median

\log_{2}(\text{unwrapped length})

versus wrapped length. Each point represents the median over all elements at that wrapped length.

Figure 4. Median wrapped length versus depth.

Figure 5. Median

\log_{2}(\text{unwrapped length})

versus depth. The approximately linear relationship indicates exponential growth of unwrapped length with depth.

Regime	$\log\|w\|_{G}$ vs depth	$\|w\|_{G^{\prime}\setminus\{w\}}$ vs depth	$\log\|w\|_{G}$ vs $\|w\|_{G^{\prime}\setminus\{w\}}$	Parsimony
$A_{n}$ , log density	Linear	Flat ∗	Degenerate ∗	Yes
$A_{n}$ , Waring	Linear	Flat	Degenerate	No
$A_{n}$ , double-log	Exponential	Doubly exp.	Logarithmic	Yes
$F_{n}$ , polynomial	Degenerate	Degenerate	Logarithmic	Yes
$F_{n}$ , probabilistic	Linear	Quadratic	Concave ( $\sqrt{\cdot}$ )	No

Table 2. Predicted relationships among

\log|w|_{G}

(log unwrapped length),

|w|_{G^{\prime}\setminus\{w\}}

(wrapped length), and depth for each monoid regime. Measurements are restricted to elements of

G^{\prime}=G\cup M

. “Degenerate” means the independent variable (i.e., the “x” in “y vs x”) is bounded. The asterisk (

\ast

) indicates that if a generic element of the monoid is considered then Flat

\rightarrow

Linear and Degenerate

\rightarrow

Linear; see 3.7.6 for discussion.

	$G$	$G^{\prime}\setminus\{u\}$
$S$	$\|S\|_{G}$	$\|S\|_{G^{\prime}\setminus\{u\}}$
$B$	$\|B\|_{G}$	$\|B\|_{G^{\prime}\setminus\{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^{\prime}\setminus\{u\}

column measures deductive compression.

Mathematical Reasoning

Mathematical reasoning studies how AI systems solve problems, construct proofs, use tools, and discover or verify mathematical results.

See all 151 papers

Learning to Discover Interesting Mathematics
Sep 23, 2026Niket Patel, Ahmad Rammal, Amaury Hayat +2Automated Theorem Proving Lean Theorem Proving
New York University · CERMICS, ENPC, Institut Polytechnique de Paris
TheoremGraph: Bridging Formal and Informal Mathematics
Jun 24, 2026Simon Kurgan, Evan Wang, Eric Leonen +6KG Construction Graph-Based Retrieval
University of Washington Math AI Lab
ResearchMath-14K: Scaling Research-Level Mathematics via Agents
May 27, 2026Guijin Son, Seungyeop Yi, Minju Gwak +3Supervised Fine-Tuning LLM Mathematical Reasoning
Seoul National University · OneLineAI · Yonsei University

Sep 23, 2026J/K move · Enter open · S save

Learning to Discover Interesting Mathematics

Niket Patel, Ahmad Rammal, Amaury Hayat, Remi Munos+1

New York University · CERMICS, ENPC, Institut Polytechnique de Paris

Automated Theorem Proving Lean Theorem Proving Large Language Model-Guided Scientific Discovery AI-Assisted Mathematical Discovery Large Language Model-Guided Theorem Proving

Open paper AskPDF arXiv

Recently, Large Language Models (LLMs) have been increasingly able to solve advanced mathematical problems, including many that have been open for decades. This opens the door to expansion of mathematical knowledge at unprecedented scale. Yet, while LLMs may be able to conjecture and prove more and more theorems, it remains open whether this new mathematical knowledge is interesting or useful. We define intrinsic interestingness of a theorem as the ratio between the length of its proof and the length of its statement. We show that this correlates strongly with an extrinsic measure of the downstream utility of a theorem. We identify the difficulty of a proof conditioned on a set of premises as a useful primitive for computing these metrics, and train a 27B model that predicts proof difficulty more accurately than frontier general-purpose models. Optimizing for our metric creates a model capable of producing more interesting theorems, while also reducing substantial or full overlap with Mathlib from 91.9% to 30.6%, showcasing the creation of more out-of-distribution math. We show that our system can generate candidate theorems, select the most interesting among them, and iteratively build on a self-expanding mathematical library. These metrics provide a practical and quantifiable signal for ranking conjectures and guiding proof search within formal mathematical libraries. Our framework provides a path towards self-expanding, machine-verified mathematical libraries that can choose worthwhile statements without relying on human-supplied targets.

Abstract

Mathematical Reasoning

Explore similar work

Learning to Discover Interesting Mathematics

TheoremGraph: Bridging Formal and Informal Mathematics

ResearchMath-14K: Scaling Research-Level Mathematics via Agents