SqueezeBench: Saturation-Resilient Evaluation of Mathematical Capability

Pablo Manrique; Hai Xia; Stefan Szeider

cs.AIOct 9, 2026

SqueezeBench: Saturation-Resilient Evaluation of Mathematical Capability

Authors: Pablo Manrique, Hai Xia, Stefan Szeider

Organizations: Algorithms and Complexity Group TU Wien, Vienna, Austria

Abstract

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.

Figures & tables

Panel of Figure 1 — Figure 1: One version step: trusted files written by squeeze (solid), untrusted submission (dashed).

Panel of Figure 2 — Figure 2: Every accepted record for the Golomb ruler problem. Colors run from light for the oldest version to dark for the newest, the standing record is drawn thick, and each version is at least as good as its predecessor at every $n$ , which its submission proved. (a) The lower records for $n\leq 100$ : the seed $\binom{n}{2}$ (dashed) and versions V001–V008, which differ only in lower-order terms and overlap at this scale. Writing $l_{k}$ for version V00 $k$ of the lower record, the inset shows the gain $l_{k}(n)-l_{1}(n)$ of each later version over V001, for $k=2,\dots,8$ ( $k=8$ drawn thick). (b) The upper records for $n\leq 40$ , from the seed (dashed) to the standing record V013.

	Known	Moves	Non-reg.	Target	2-sided	Cited	Check	Mode	Sub.
Benchmarks: A system is scored against mathematical problems
miniF2F, ProofNet, PutnamBench, FormalMATH, Lean Workbook	yes	no	NA	prop.	NA	NA	proof	auto	proof
CombiBench	yes	no	NA	prop.	NA	NA	proof	auto	answer + proof
SorryDB, ArXivLean	yes c	no	NA	prop.	NA	NA	proof	auto	proof
FrontierMath Erdős	no	no	NA	prop.	NA	NA	proof	auto	proof
Formal Conjectures	no	no	no	function a	yes	yes d	proof	auto	answer term a

Table 1: Mathematical benchmarks and record archives. NA marks a system that maintains no standing record. Only where a submission replaces a total function can a replacement be tighter at one

n

and looser at another, and only SqueezeBench both replaces functions and proves that the replacement never regresses. Notes: a Formal Conjectures’ function-valued bound goals are unproved ( := by sorry ) and asymptotic, so improving a single

n

earns no credit. b HorizonMath compares against a fixed value in data/baselines.json ; beating it does not replace it. c SorryDB and ArXivLean refresh the task stream: an answer key exists, but is kept fresh. d Formal Conjectures’ anchors c1a_lower_bound and c1a_upper_bound both carry sorry while tagged as solved. e FrontierShift shows a gap on some pages, but only its upper side is a maintained record. Sources. PutnamBench ( Tsoukalas et al., 2024 ) , FormalMATH ( Yu et al., 2025 ) , Lean Workbook ( Ying et al., 2024 ) , CombiBench ( Liu et al., 2025 ) , SorryDB ( Letson et al., 2026 ) , ArXivLean ( Gehrunger et al., 2026 ) , FM: Open Problems ( Epoch AI, 2026 ) , Covering ( Acerbi, 2026 ) , Grassl ( Grassl, 2026 ) , EinsteinArena ( Bianchi et al., 2026 ) . The remaining systems are cited above.

Problem	$f$ counts	Domain	Standing lower record	Standing upper record
Additive combinatorics
Cap set	largest subset of $\mathbb{F}_{3}^{n}$ with no three collinear points	$n\geq 1$	growth $112^{1/6}\approx 2.196$ (extended products of caps)	$O(2.756^{n})$ (Ellenberg–Gijswijt) $\star$
Roth	largest subset of $\{0,\dots,n-1\}$ with no 3-term progression	$n\geq 1$	$\Theta(n^{0.638})$ ; exact for $n\leq 209$	$4n/11+O(1)$ (Moser)
Ruzsa–Szemerédi	most triangles in an $n$ -vertex graph whose every edge lies in exactly one triangle	$n\geq 3$	$\Theta(n^{1.716})$ (from cap sets)	$n^{2}/18+O(n)$ , smaller for $n\geq 33$ (counting) $\dagger$
Golomb	shortest ruler with $n$ marks and all differences distinct	$n\geq 1$	$n^{2}-2n^{3/2}+O(n)$ $\star$	$\approx n^{2}$ (Singer) $\star$ ; best known for $n\leq 100$
Extremal graph theory

Table 2: The ten problems and their standing records after the runs of Section 5 . Seed records are omitted; each is the simplest provable bound, and several are trivial. Golomb is a minimization problem, and its upper record and lower record are the construction and impossibility argument, respectively. For all other problems, constructions give the lower record. ⋆ matches the leading term of the best published bound, or its base if the bound is exponential, in that direction. † matches the best elementary bound; the published frontier uses the triangle removal lemma. Unmarked records are asymptotically behind the literature.

Explore similar work

Apr 8, 2026

Riemann-Bench: A Benchmark for Moonshot Mathematics

Recent AI systems have achieved gold-medal-level performance on the International Mathematical Olympiad, demonstrating remarkable proficiency at competition-style problem solving. However, competition mathematics represents only a narrow slice of mathematical reasoning: problems are drawn from limited domains, require minimal advanced machinery, and can often reward insightful tricks over deep theoretical knowledge. We introduce Riemann-Bench, a private benchmark of expert-curated problems designed to evaluate AI systems on research-level mathematics that goes far beyond the olympiad frontier. Problems are authored by Ivy League mathematics professors, graduate students, and PhD-holding IMO medalists, and routinely took their authors weeks to solve independently. Each problem undergoes double-blind verification by two independent domain experts who must solve the problem from scratch, and yields a unique, closed-form solution assessed by programmatic verifiers. We evaluate frontier models as unconstrained research agents, with full access to coding tools, search, and open-ended reasoning, using an unbiased statistical estimator computed over 100 independent runs per problem. Our results reveal that all frontier models currently score below 10%, exposing a substantial gap between olympiad-level problem solving and genuine research-level mathematical reasoning. By keeping the benchmark fully private, we ensure that measured performance reflects authentic mathematical capability rather than memorization of training data.

Suhaas Garre, Erik Knutsen, Sushant Mehta +1

Surge AI

Mathematical Reasoning Benchmarks Benchmark Design AI Agent Benchmarks LLM Mathematical Reasoning

Ask PDF

May 17, 2026

CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean

Formal theorem-proving benchmarks enable mechanically verifiable evaluation of mathematical reasoning in large language models. However, existing benchmarks mainly focus on Olympiad-style problems and algebraic domains, leaving computational and applied mathematics underrepresented. We introduce CAM-Bench, a Lean 4 theorem-proving benchmark of 1,000 Lean proof targets in computational and applied mathematics, with coverage spanning optimization, numerical linear algebra, and numerical analysis. These problems are adapted from textbook exercises and often depend on locally introduced definitions, notation, algorithms, and elementary results. To construct CAM-Bench, we develop a dependency-recovery pipeline that reconstructs the local textbook context needed to state each problem faithfully. It then normalizes each problem into a standalone informal theorem and translates it into a Lean target. We validate the resulting formal problems through Lean compilation and semantic review, checking both formal correctness and semantic alignment with the original exercises. For each problem, we release the raw exercise, recovered context, normalized informal theorem, and final Lean target. CAM-Bench complements existing formal mathematics benchmarks by targeting applied mathematics problems that rely on textbook concepts and elementary theorems, many of which are not directly available as standard Mathlib4 lemmas. We evaluate widely used large language models and formalization agents on CAM-Bench, and analyze common failure modes in tracking local assumptions, applying elementary results, decomposing proofs, and maintaining long-horizon control in Lean.

Wentao Long, Yunfei Zhang, Chenyi Li +3

Fudan University · Qingdao University · Peking University +1

Mathematical Reasoning Benchmarks Benchmark Construction Lean Theorem Proving

Ask PDF

Feb 27, 2026

LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics

We present a new approach for benchmarking Large Language Model (LLM) capabilities on research-level mathematics. Existing benchmarks largely rely on static, hand-curated sets of contest or textbook-style problems as proxies for mathematical research. Instead, we establish an updatable benchmark evaluating models directly on the latest research results in mathematics. This consists of an automatic pipeline that extracts lemmas from arXiv and rewrites them into self-contained statements by making all assumptions and required definitions explicit. It results in a benchmark that can be updated regularly with new problems taken directly from human mathematical research, while previous instances can be used for training without compromising future evaluations. We benchmark current state-of-the-art LLMs, which obtain around 10-15

\%

accuracy in theorem proving (pass@1) depending on the model, showing that there is currently a large margin of progression for LLMs to reach human-level proving capabilities in a research context.

Antoine Peyronnet, Fabian Gloeckle, Amaury Hayat

1Ecole Normale Superieure de Rennes · 2Ecole des Ponts Paris · 3Korean Institute for Advanced Study

Mathematical Reasoning Benchmarks Automated Theorem Proving LLM Mathematical Reasoning

Ask PDF