Leanify: Verified Proof Compression and Reusable Lemma Discovery

Language models can prove difficult mathematical statements, but their proofs still need to be organized for understanding and reuse. It has been argued that mathematics advances by compression: concepts and theorems turn long deductions into reusable arguments. We formulate proof compression as a verifiable task: shorten Lean proof collections while preserving their original statements. Our agents compress the Lean proofs of the permanent lower bound and of the counterexamples to the compactness conjecture from OpenAI's Ten Advances in Mathematics and Theoretical Computer Science by 94.2% and up to 99.2%, respectively, under our proof-term size metric. For the permanent proof, compression also reduces the number of required intermediate theorems and shortens model-generated mathematical explanations. Using a lemma-discovery pipeline, we observe two scaling trends: later compression stages yield a larger share of lemmas judged non-trivial by a language model, and compressing more related Fermat's Last Theorem results together yields wider lemma reuse. These trends suggest that scaling compression may uncover more reusable mathematical arguments. We therefore release Leanify as a benchmark to test this possibility at scale.