SqueezeBench: A Saturation-Resilient Benchmark for AI Mathematical Capability

Why Existing Math Benchmarks Are Failing

AI progress in mathematics has been remarkable — but measuring that progress has become a challenge in itself. Traditional math benchmarks face two fundamental traps: those built on solved problems get saturated quickly, losing their discriminative power once frontier models answer everything correctly; those built on unsolved open problems can only be conquered once, making repeated measurement impossible.

In other words, when AI systems approach or exceed the expectations of benchmark designers, these evaluation tools rapidly lose their value. Researchers need an evaluation mechanism that can evolve alongside growing capabilities. SqueezeBench is designed precisely to address this pain point.

SqueezeBench's Core Mechanism: Success Raises the Bar

SqueezeBench's design philosophy can be summed up in one sentence — solving a problem doesn't remove it; it raises the bar for it. This "saturation-resilient" property is what sets it apart from traditional benchmarks.

Concretely, each problem corresponds to an integer function $f(n)$, whose values are only known for small $n$. The benchmark maintains a lower-bound record and an upper-bound record for each function. A "record" is a computable Lean function accompanied by a machine-verifiable proof that it genuinely bounds $f$.

When someone submits a new result, they must simultaneously prove three things: that the new function truly bounds $f$; that it is no worse than the current record at any $n$; and that it strictly improves upon the current record at least at some $n$. Once accepted, this new function becomes the new record — and the next submitter must surpass it to be recognized.

Choosing Both Bounds and Proofs

This system has an interesting property: it requires participants to choose not just the "answer" (a tighter bound) but also the "proof." Improvements can occur at a single point $n$, or manifest as a better growth rate overall. At every $n$, the gap between the upper and lower records intuitively reflects how far the certified bounds are from pinning down the true value of $f(n)$.

Dual Lean Kernel Verification: No Human Judges Required

Another engineering highlight of SqueezeBench is its verification mechanism. Every proof is checked by two independent Lean kernels, meaning the entire audit of mathematical correctness requires no human judges. This dramatically reduces subjectivity and maintenance overhead.

Of course, automated verification must also guard against cheating. The system actively rejects functions that "compute" $f$ by exhaustive search over small $n$ — this is memorization, not genuine mathematical reasoning. Maintainers' responsibilities are limited to reading submission reports and watching for similar exhaustive-search tricks at larger values of $n$.

This architecture — machine verification as the primary layer, human spot-checks as a secondary layer — keeps the benchmark credible and sustainable at scale.

Lean is an interactive theorem prover developed by Microsoft Research and widely used in the formal mathematics community. Its core idea is to use a strict type theory as the logical foundation, representing mathematical propositions as types and proofs as terms of those types, with the computer kernel mechanically checking the validity of each inference step. Unlike traditional "human review," once Lean's kernel accepts a proof, its correctness is mechanically guaranteed within that logical system — no human judgment or trust required. SqueezeBench uses two independent Lean kernels for cross-validation as an additional defensive measure: since the two kernels are independently implemented, the probability that both accept a proof containing a shared error is extremely low, further strengthening the credibility of verification results. This is why the entire evaluation pipeline can operate without human judges — the final authority on mathematical correctness is fully delegated to auditable machine logic.

Experimental Results: Frontier Model Performance and Limitations

The research team released ten problems from the field of extremal combinatorics, along with twenty proven initial records and onboarding tools.

As a baseline test, an agent based on one frontier language model — given up to one hour per record — had 82 submissions accepted, improving all records, though none of the improvements exceeded the scope of published literature. Subsequently, agents based on two newer models continued from those records, yielding 60 more accepted submissions and improving 19 out of 20 records.

This data reveals two layers of insight. On one hand, frontier models genuinely possess the ability to continuously advance mathematical boundaries, and newer-generation models can build on the results of older ones — validating the benchmark's "relay-style" evolutionary design. On the other hand, a sobering fact remains: in eight of the ten problems, at least one record still lags behind the best published bounds in an asymptotic sense.

In other words, even the strongest current AI agents have not yet matched the best results from the human mathematical community under rigorous machine-verified standards. This provides a more honest measuring stick for assessing AI's true mathematical capability.

Extremal combinatorics is a branch of combinatorics focused on this core question: within discrete structures (graphs, set systems, sequences, etc.) satisfying some constraint, what is the maximum or minimum value of a given parameter? A classic example is the Turán problem: "What is the maximum number of edges a graph on $n$ vertices can have without containing a triangle?" Such problems are characterized by answers that are functions of $n$, where upper and lower bounds often come from entirely different proof techniques, and closing the asymptotic gap between them is frequently very difficult. This makes extremal combinatorics problems a natural fit for SqueezeBench's framework of maintaining and tightening bounds — they won't be fully resolved in one stroke, yet can see steady incremental progress through improved constructions or proof techniques. This makes them an ideal domain for testing AI's sustained mathematical reasoning ability.

Implications for AI Evaluation Paradigms

SqueezeBench represents a noteworthy shift in evaluation thinking. It transforms a static "problem bank" into a dynamic, never-saturating "arena" where every success becomes the starting point for the next challenge. This design is a natural fit for AI systems whose capabilities continue to grow, avoiding the awkward cycle of benchmarks repeatedly becoming obsolete and needing to be rebuilt.

More importantly, machine-verifiable proofs combined with dual-kernel cross-checking establish a rigorous standard of trustworthiness for AI mathematical capability assessment. Compared to tests that rely on human scoring or can be gamed by memorization, SqueezeBench advances the bar on both objectivity and cheat-resistance. As AI continues to evolve in formal mathematics, saturation-resilient, self-evolving evaluation frameworks like this may well become critical infrastructure for future research.