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

This post is an in-depth Chinese-language analysis of Fields Medalist Michael Freedman's paper *Compression Is All You Need*, which makes a striking claim: compression is the core mechanism by which mathematical knowledge is constructed. The paper uses an elegant algebraic model to address three long-standing questions: How do humans build mathematical knowledge? What fundamentally distinguishes human mathematics from formal logical mathematics? And how should human mathematicians collaborate with AI in the future?

Mathematical Foundations of Compression Theory

Freedman models mathematical reasoning as symbol strings and measures compression via macros. A proof is a raw symbol string; definitions, lemmas, and theorems are names for substrings—macros. Using a macro compresses the expression while its expansion recovers the full information.

Free Commutative vs. Free Non-Commutative Monoids

Freedman compares two extremes using finitely generated monoids:

• Free commutative monoid \(A_n\): generators can be freely reordered; elements behave like n-dimensional natural number vectors, and ball volume grows polynomially with radius. This models order-independent mathematical objects (e.g., addition, set unions).
• Free non-commutative monoid \(F_n\): generators concatenate strictly in order; there are \(n^r\) strings of length \(r\), so ball volume grows exponentially. This models order-dependent reasoning, such as programs or formal proofs.

Macro Density and Extension Power

Introducing macros amounts to adding redundant generators. The theory reveals:

• In \(A_n\), a logarithmically sparse macro set (e.g., powers of 10 in decimal positional notation) suffices for exponential growth in expressive power.
• In \(F_n\), even polynomial-density macro sets yield only linear improvement; significantly exceeding linear growth requires near-maximal macro density.
• At polynomial density, \(A_n\) can achieve infinite extension (every element finitely expressible), while \(F_n\) remains limited even with exponentially dense macro sets.

Predictions and MathLib Empirics

Freedman proposes two predictions for human mathematics:

1. Expanded length (fully expanded symbol count) grows exponentially with depth (nesting level) and packaged length (raw definition size). 2. Packaged length stays roughly constant across depths.

Formalized mathematics predicts the opposite: near-linear expansion and growing packaged length.

The team tested these on MathLib, a large Lean 4 library with hundreds of thousands of definitions, lemmas, and theorems. Treating entries as nodes in a DAG and computing depth, packaged length, and expanded length, the results strongly supported the theory:

• Expanded length shows a significant exponential relationship with depth and packaged length.
• Packaged length distributions are approximately constant across depths.

These findings match the \(A_n\) model and contradict the \(F_n\) model—human mathematics is genuinely "soft and compressible."

Human Mathematics vs. Formalized Mathematics

• Growth: Formal systems grow linearly and exhaustively; human mathematics achieves exponential leverage from a small set of foundational concepts.
• Structure: Formal proofs are flat strings; human mathematics has a hierarchical structure of deeply nested, reusable concepts.
• Complexity: In formal systems, step complexity grows with depth; in human mathematics, each definition stays locally simple regardless of nesting—a local simplicity principle.

Thus human mathematics is not merely a subset of formal mathematics but a compressed, filtered distillation of it: incompressible, meaningless formal deductions are naturally excluded. This explains how mathematics can be vast yet graspable by human minds.

Philosophical Significance

• Understanding is compression: To understand is to find a concise representation preserving essential features. Deeper compression means deeper understanding.
• A universal principle: The idea connects to Shannon's information theory, the Compression Thesis in AI (prediction as compression, e.g., next-token prediction in LLMs), and the Free Energy Principle (self-organizing systems minimize prediction error, i.e., maximize compression).
• Discovery vs. invention: From the compression view, mathematics is closer to discovery—mathematicians explore the infinite logical space for compressible, meaningful structures and bring them back in concise form.
• Progress: Mathematical breakthroughs (calculus, group theory) can be seen as jumps in compression paradigms.

Conclusion and Outlook

Freedman's theory powerfully supports compression as the core mechanism of mathematical knowledge, clarifying the human/formal divide and enriching philosophy of mathematics. For AI collaboration, it suggests:

• AI should go beyond mechanically generating proofs to discovering compressible structures—the macros that most simplify reasoning—acting as a "mathematical explorer."
• AI mathematical ability could be measured by its compression depth rather than problem counts alone.
• Human-AI collaboration may eventually probe "non-compressed regions" of mathematics—structures too complex or uninteresting for humans but meaningful to higher intelligences—reshaping the boundaries of mathematical cognition.