Compression is all you need: Modeling Mathematics
New research argues human math is defined by compressibility, with profound implications for AI theorem provers.
A team of researchers including Michael H. Freedman and Michael Mulligan has published a provocative preprint titled 'Compression is all you need: Modeling Mathematics.' The paper posits a fundamental distinction between the vast, formal universe of all valid mathematical deductions (FM) and the tiny, curated subset that humans actually discover and value (HM). The core thesis is that HM is uniquely characterized by its high compressibility through hierarchical structures like definitions, lemmas, and theorems.
To model this, the authors use monoids, where a mathematical statement is a string of symbols and a theorem is a 'macro' that compresses it. They analyze two models: free abelian monoids (A_n) and free non-abelian monoids (F_n). Their analysis shows that in A_n, a sparse set of macros yields exponential expressive growth, while in F_n, achieving superlinear growth requires an impractically dense macro set. They then test these models against MathLib, a large formal library written in the Lean 4 proof assistant, treating it as a proxy for HM.
The empirical results are striking. They measure the 'unwrapped length' (primitive symbols after full expansion) and 'wrapped length' (tokens in the compact definition) of MathLib elements. They found unwrapped length grows exponentially with both depth and wrapped length, while wrapped length remains roughly constant across depths. This pattern is consistent with the abelian monoid (A_n) model and inconsistent with the non-abelian (F_n) model, supporting the idea that HM occupies a polynomially-growing region within an exponentially vast space.
Finally, the paper discusses practical implications for AI-driven automated reasoning. It suggests that compression metrics and PageRank-style analysis of mathematical dependency graphs could be used to quantify 'mathematical interest' and guide AI systems—like those built on Lean or other proof assistants—away from the exponentially large, incompressible wilderness of FM and toward the compressible, human-like regions where meaningful discovery occurs.
- The paper argues human mathematics (HM) is distinguished from all formal mathematics (FM) by its compressibility via hierarchical definitions and theorems.
- Modeling with monoids shows a sparse macro set in an abelian structure yields exponential growth, matching empirical data from the Lean 4 MathLib library.
- The findings suggest AI theorem provers should use compression metrics to target 'interesting,' human-like mathematics, potentially revolutionizing automated reasoning.
Why It Matters
This provides a formal, testable theory to guide AI theorem provers away from meaningless formal searches and toward human-like mathematical discovery.