# SqueezeBench: Saturation-Resilient Evaluation of Mathematical Capability

arXiv: https://arxiv.org/abs/2610.13461 · HTML: https://mlsanity.com/paper/2610.13461/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 15 of its 47 references that are in the map.
- First posted on arXiv 9 Oct 2026.

## Builds on (most cited first, 15 of 15)

- [AlphaEvolve: A coding agent for scientific and algorithmic discovery](https://mlsanity.com/paper/2506.13131/) (2025)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models](https://mlsanity.com/paper/2505.02735/) (2025)
- [PatternBoost: Constructions in Mathematics with a Little Help from AI](https://mlsanity.com/paper/2411.00566/) (2024)
- [When AI Benchmarks Plateau: A Systematic Study of Benchmark Saturation](https://mlsanity.com/paper/2602.16763/) (2026)
- [Semi-Autonomous Mathematics Discovery with Gemini: A Case Study on the ErdHos Problems](https://mlsanity.com/paper/2601.22401/) (2026)
- [CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics](https://mlsanity.com/paper/2505.03171/) (2025)
- [Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics](https://mlsanity.com/paper/2605.13171/) (2026)
- [Harnessing the Collective Intelligence of AI Agents in the Wild for New Discoveries](https://mlsanity.com/paper/2606.10402/) (2026)
- [SorryDB: Can AI Provers Complete Real-World Lean Theorems?](https://mlsanity.com/paper/2603.02668/) (2026)

## Abstract (arXiv)

AI systems are making rapid progress in mathematics, but this progress is hard to measure. Benchmarks of solved problems saturate, and in benchmarks of open problems each problem can be resolved for the first time only once. We present SqueezeBench, a benchmark that is resilient to saturation: a success raises the bar instead of removing the problem. Each problem fixes an integer function f(n) whose values are known only for small n, and the benchmark keeps a lower and an upper record on it. A record is a computable Lean function with a machine-checked proof that it bounds f. A submission proposes a new function and proves that it bounds f, that it is no worse than the current record at any n, and that it is strictly better at some n. Once accepted, it becomes the record that the next submission has to beat. The system thus chooses the bound as well as its proof, and it may improve the record at a single n or its growth rate. At every n, the gap between the two records shows how far the certified bounds are from determining f(n). Every proof is checked by two independent Lean kernels, so no referee needs to check the mathematics. The checks also reject a function that computes f by exhaustive search at small n, and a maintainer only reads the submitter's report and looks for such a search at larger n. We release ten problems from extremal combinatorics with twenty proved initial records and the admission tools. As a baseline, agents based on a frontier language model, with at most one hour per record, had 82 submissions accepted and improved every record, without going beyond the published literature. Agents based on two newer models then started from these records, had 60 more submissions accepted and improved 19 of the 20 records again. For eight of the ten problems, at least one record is still asymptotically behind the best published bound.