The Compression Principle: Why Human Mathematics Outperforms Formal Systems

This research reveals a fundamental insight: human mathematics achieves exponential compression of logical complexity through hierarchical abstraction, enabling practitioners to navigate problems that would otherwise explode exponentially. By analyzing Lean's Mathlib library containing 500,000 mathematical elements, researchers demonstrated that while complete formal derivations grow exponentially with depth, human notation remains linear—suggesting mathematics progresses by discovering increasingly compressible logical structures. These findings offer a new framework for improving AI theorem proving through compression-based metrics for premise selection.