The frontier of mathematics will soon reach far beyond the subset that human minds discover. Working memory of ~10 is a very strong constraint on ape brains! 🧠🐒 Compression is all you need: Modeling mathematics Abstract: The mathematics humans discover and value (“human math”) is a vanishingly small subset of all valid deductions (“formal math”). I’ll argue that human math is distinguished by its compressibility through hierarchically nested definitions and theorems, like a polynomial-growth space rather than the exponential-growth space one might expect when proofs are viewed as strings of symbols. The argument combines toy monoid models with an empirical analysis of MathLib, a large Lean library of formalized mathematics we treat as a proxy for human math. I’ll close with how compression itself can serve as a measure of mathematical interest, giving agents a sense of direction toward where human math lives.