AI systems are advancing rapidly in mathematics, yet measuring this progress is challenging. Existing solved‑problem benchmarks quickly saturate, and open‑problem benchmarks allow each problem to be resolved only once. We introduce SqueezeBench, a benchmark resilient to saturation: every 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$. The benchmark keeps a lower and an upper record for this function. A record is a computable Lean function accompanied by a machine‑checked proof that it bounds $f$. A submission must propose a new function and prove that it is no worse than the current record for all $n$, and strictly better for some $n$. Once accepted, the new function becomes the record that the next submission must beat. Thus the system selects both the bound and its proof, allowing improvement at a single $n$ or in the growth rate.\ \ At every $n$, the gap between the two records indicates how far certified bounds are from determining $f(n)$. All proofs are verified by two independent Lean kernels, eliminating the need for human referees. The checks also reject functions that compute $f$ by exhaustive search on small $n$, so maintainers only read the submitter’s report and look for such searches at larger $n$. We release ten extremal combinatorics problems, twenty initial proved records, and the submission tools. As a baseline, agents based on a frontier language model, limited to one hour per record, made 82 accepted submissions that improved every record, though none surpassed the published literature. Agents based on two newer models then started from these records, made 60 more accepted submissions, and improved 19 of the 20 records again. For eight of the ten problems, at least one record remains asymptotically behind the best published bound.\ \ Review