Michael Freedman's 'Compression Is All You Need': Compression as the Core Mechanism of Mathematical Knowledge

Forum topic · ✨步子哥 · 2026-04-18

Summary

This article interprets Fields Medalist Michael Freedman's paper 'Compression Is All You Need,' which argues that compression is the central mechanism by which mathematical knowledge is built. Freedman models mathematical reasoning as symbol strings and introduces 'macros' (names for definitions, lemmas, and theorems) to measure compression. Comparing free commutative monoids with free non-commutative monoids, the theory predicts that in human mathematics, a concept's fully expanded length grows exponentially with its depth and packed length, while packed length stays roughly constant across depths. Empirical analysis of MathLib, a large Lean 4 mathematical library, strongly supports these predictions, suggesting human mathematics resembles a compressible commutative model rather than an incompressible formal one. The article also explores the philosophical implications: compression as understanding, connections to the free energy principle and large language models, and prospects for human-AI collaboration in discovering compressible mathematical structures.

Introduction

In his paper *Compression Is All You Need*, Fields Medalist Michael Freedman makes a striking claim: compression is the core mechanism by which mathematical knowledge is constructed. Using an elegant algebraic model, the paper addresses three long-standing questions: How do we build mathematical knowledge? What is the essential difference between human mathematics and formal logic-based mathematics? How should human mathematicians collaborate with AI in the future? Freedman's answer rests on a single concept—compression.

Mathematical Foundations of the Compression Theory

Freedman abstracts mathematical reasoning as symbol strings and measures compression via macros: definitions, lemmas, and theorems are names for substrings of the raw symbol string. Introducing a macro compresses an expression; expanding it restores the original information.

Free Commutative vs. Free Non-Commutative Monoids

The model compares two extremes:

Free commutative monoid $$A_n$$ : generators can be reordered; elements are $$n$$ -dimensional vectors of natural numbers; ball volume grows polynomially with radius. This models order-independent mathematical objects.
Free non-commutative monoid $$F_n$$ : generators are strictly ordered; there are $$n^r$$ strings of length $$r$$ , so ball volume grows exponentially. This models order-dependent reasoning, such as formal proofs or code.

Density of Macro Sets and Expansion Power

Adding a macro is like adding a redundant generator. Introducing 10, 100, 1000, ... in $\mathbb{N}$ recreates decimal positional notation. Key findings:

Log-sparsity suffices in $$A_n$$ : a logarithmically sparse macro set achieves exponential expansion of expressive power.
Near-maximal density required in $$F_n$$ : only polynomially dense macro sets yield linear improvement; significant growth beyond linear requires nearly maximal macro density.
Extreme cases: at polynomial density, $$A_n$$ can achieve infinite expansion; even exponential density in $$F_n$$ only slightly exceeds linear growth.

Predictions and Empirical Validation via MathLib

Freedman makes two predictions for human mathematics:

1. Expanded length grows exponentially with depth and packed length: more foundational definitions support a larger superstructure. 2. Packed length is roughly constant across depths: each definition's intrinsic complexity stays stable no matter how deep the nesting.

Formal mathematics would predict instead a roughly linear relationship and growing packed length.

To test this, Freedman's team used MathLib, a large Lean 4 library with hundreds of thousands of entries, constructing a directed acyclic graph of dependencies and computing each node's depth, packed length, and expanded length. Results strongly confirmed the theory:

Expanded length shows a clear exponential relationship with depth and packed length.
Packed length distributions remain approximately constant across depths.

These results align with the $$A_n$$ model and contradict the $$F_n$$ model, suggesting human mathematics is genuinely "soft and compressible."

Human Mathematics vs. Formal Mathematics

Formal mathematics is the totality of all valid deductions under given axioms and rules—an enormous space, mostly untouched by humans (as Gödel's incompleteness theorems imply).
Human mathematics is a tiny subset whose distinctiveness lies in compressibility: layered definitions, lemmas, and theorems form reusable macros that dramatically reduce the symbols needed to express new ideas.

Key differences:

Growth mode: formal systems grow linearly and exhaustively; human mathematics achieves exponential expansion through compression.
Structure: formal proofs are flat strings; human mathematics has a deep, modular, hierarchical concept network.
Complexity distribution: in formal systems, per-step complexity grows with depth; in human mathematics, each definition stays locally simple regardless of nesting depth.

Thus human mathematics is not merely a subset of formal mathematics but a compression-filtered distillation of it—only compressible, meaningful structures are retained, which is why the vast edifice of mathematics remains graspable by human minds.

Philosophical Significance

Compression is understanding: to understand a phenomenon is to find a concise description preserving its essential features. In mathematics, deeper compression equals deeper understanding.
Universality of compression: this connects to Shannon's information theory, the compression thesis in AI (understanding as prediction, e.g., large language models compressing text), and the Free Energy Principle, under which self-organizing systems minimize prediction error—equivalently, maximize compression. In this view, mathematics is the extreme manifestation of a universal cognitive principle.
New perspectives on classic questions:
*Invention vs. discovery*: mathematics is closer to discovery—mathematicians are explorers finding compressible, meaningful structures in an infinite logical space.
*Objectivity*: compressible structures exist objectively; human mathematics is a compression mapping of them, shaped by cognitive limits and interests.
*Progress*: mathematical progress is the deepening of compression—breakthroughs like calculus and group theory are compression paradigm shifts.

Conclusion and Outlook

Freedman's *Compression Is All You Need* provides rigorous modeling and empirical support for compression as the core mechanism of mathematical knowledge construction, clarifying the human/formal distinction and enriching philosophy of mathematics. For AI-human collaboration, it suggests AI should not merely generate proofs but discover compressible structures—acting as a mathematical explorer. AI mathematical ability could be measured by compression depth rather than problem count. Most excitingly, collaboration may let us explore the non-compressible regions beyond human mathematics—structures too complex or uninteresting for humans but meaningful to more advanced intelligences—redefining the boundaries of mathematical cognition.