Compression is all you need: Modeling Mathematics

Computer Science > Artificial Intelligence [Submitted on 20 Mar 2026] Compression is all you need: Modeling Mathematics Vitaly Aksenov, Eve Bodnia, Michael H. Freedman, Michael Mulligan 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. Comments: 28 pages, 5 figures, 1 appendix Subjects: Artificial Intelligence (cs.AI); Logic (math.LO) Cite as: arXiv:2603.20396 [cs.AI]   (or arXiv:2603.20396v1 [cs.AI] for this version)   https://doi.org/10.48550/arXiv.2603.20396 Focus to learn more Submission history From: Michael Mulligan [view email] [v1] Fri, 20 Mar 2026 18:16:27 UTC (99 KB) Access Paper: HTML (experimental) view license Current browse context: cs.AI < prev   |   next > new | recent | 2026-03 Change to browse by: cs math math.LO References & Citations NASA ADS Google Scholar Semantic Scholar Export BibTeX Citation Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Demos Related Papers About arXivLabs Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)