LemmaBench: The Math World's "Liveness Test" That Turns LLM Champions Back Into Newcomers

> TL;DR: A team from ENS Rennes and École des Ponts/IP Paris built a "research-paper harvesting machine"—an automated pipeline that extracts lemmas from the latest arXiv papers each week, completes their scattered definitions and assumptions, and turns them into self-contained standalone propositions. Top LLMs asked to prove them achieve pass@1 accuracy of only 10-15%. The leaderboard mythology of competition math shatters against research-level mathematics.

| Item | Details | |------|---------| | Paper | LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics | | arXiv | 2602.24173v1 | | Date | February 27, 2026 | | Team | Antoine Peyronnet (ENS Rennes · École des Ponts/IP Paris), Fabian Gloeckle (École des Ponts/IP Paris), Amaury Hayat (École des Ponts/IP Paris · Korea Institute for Advanced Study) | | Core method | Automated pipeline: arXiv scraping → LaTeX parsing → lemma extraction → dependency completion (full-context / vector retrieval) → self-containment judging (LLM-as-judge + human verification) → theorem-proving evaluation | | Models tested | GPT-5, Gemini 2.5 Pro, Gemini 3 Pro, Claude 4.5 Opus, DeepSeek-R | | Key result | Research-level lemma proving pass@1: roughly 10%-15% depending on model | | Dataset traits | Dynamically updated (refreshable weekly), contamination-resistant, historical versions usable for training without affecting future evaluations | | Coverage | Frontier branches across arXiv math categories: algebraic geometry, probability, analysis, combinatorics, etc. |

Why Static Benchmarks Are Broken

The crisis in math-reasoning benchmarks isn't new. GSM8K, MATH, and AIME were once touchstones, but as pretraining corpora ballooned into trillions of tokens, two problems loomed:

1. Data contamination — models may have seen the questions (and solutions) during training. Is a high score real understanding or memorization? 2. Distribution shift — competition and textbook problems are patterned: complete conditions, clean notation, unique answers. Real research lemmas sit mid-chain in an argument, with definitions scattered pages earlier and assumptions buried in footnotes. Understanding one may require reading the first three sections of a paper.

LemmaBench's philosophy is simple: if a model can prove a lemma mathematicians just wrote on arXiv today, it isn't reciting—because the question bank doesn't exist yet.

The Four-Step Pipeline

1. Harvest

The pipeline scrapes recent arXiv math preprints (math.AG, math.PR, etc.), extracting lemma, theorem, and proposition LaTeX environments. A second iteration added a filter: lemmas containing citations are dropped—those are restatements of known results, not new proofs.

2. Complete

Research lemmas are rarely self-contained: "condition (3.2)" might be on page 7, the definition of "function f" in Section 3, the lemma on page 9. Two completion strategies were tested:

• Full-context retrieval: feed the entire paper preceding the lemma to an LLM and ask it to find all missing definitions D and assumptions H making the lemma an independently provable statement.
• Vector retrieval: give only the lemma, use embeddings to find the most relevant passages, then extract dependencies from those.

Full-context wins decisively: GPT-5 judged 78.5% of lemmas self-contained in full-context mode vs. 49.4% with vector retrieval. Math dependencies are often long-range; embedding-based local similarity can't capture "a Section 3 definition implicitly used by a page-9 lemma."

3. Gatekeep

Completed lemmas go through LLM-as-a-judge binary verification (sufficient definitions/assumptions for independence?). Human mathematicians spot-checked: lemmas judged "self-contained" by the LLM were indeed self-contained 75.5%-96.5% of the time (depending on extraction model and mode). GPT-5 was the highest-precision gatekeeper—conservative, more false negatives, very few false positives—and became the default extractor.

4. Examine

Self-contained lemmas become problems: the model receives the lemma statement plus completed definitions/assumptions and attempts a proof, judged by an LLM judge with human spot-checks of judge reliability.

Key design: historical LemmaBench versions can be used for training without affecting future evaluations, since arXiv produces new papers weekly—cutting the train-to-test leakage channel.

What 10-15% Means

This isn't "models got 10% of math questions right"—it's "models proved 10-15% of fresh research-level lemmas." These are auxiliary results invented to push frontier theorems forward: understanding a non-standard definition, recognizing hidden structure, constructing a nontrivial auxiliary object, or combining known techniques in novel ways.

• GPT-5, Gemini 2.5 Pro / 3 Pro, Claude 4.5 Opus, DeepSeek-R — all land in the 10-15% band
• No clear winner. Top models don't separate from each other on research-level math

Three readings:

1. Optimistic: models genuinely prove some research lemmas. Not zero—basic reasoning ability exists, just unstable and unsystematic. 2. Pessimistic: an 85-90% failure rate. A theorem needing five proven lemmas has, under independence, less than a 10⁻⁵ success rate—effectively zero in practice. 3. Methodological: this exposes a domain-generalization collapse. Models hit 90%+ on competition math because those problems follow fixed patterns with a finite technique set. Research math's patterns are open, its techniques unknown, its structures must be invented. Competition-to-research is a qualitative chasm, not a quantitative gap.

Honest Uncertainties

• LLM-as-judge reliability ceiling: self-containment judging was human-validated, but proof-validity verification relies mainly on the LLM judge with only subset human checks. If judge errors are systematic (e.g., favoring constructive proofs, misjudging contradiction arguments), the 10-15% figure is biased.
• Unreported difficulty variance: arXiv lemmas range from trivial ("direct from the definition") to very hard. If the 10-15% comes mostly from trivial ones, real capability is lower.
• Cultural dependence of self-containment: what counts as "standard or classical" varies by subfield and reviewer background. Is the judge's standard stable? Undiscussed.
• Real update cadence and cost: "weekly updates" are claimed, but actual infrastructure costs (scraping, LLM calls, human checks) aren't quantified.
• Training/evaluation boundary: if training on v1-v10 improves v11 performance, is that genuine generalization or overfitting to LemmaBench's style? Needs finer ablation.

The Author's Take

LemmaBench's value lies less in the "10-15%" number than in the methodological correction. Two years of 95%+ on GSM8K, 90%+ on MATH, 80%+ on AIME fueled talk of "AI mathematicians." LemmaBench is a cold shower: those scores are real, but they measure the early stages of mathematical reasoning—pattern recognition, symbol manipulation, reproduction of known templates. Research-level math needs none of those primarily.

Dynamic evaluation isn't new (LiveCodeBench, DyVal, NPHardEval), but LemmaBench lands it in a domain traditionally very hard to automate—research-level mathematical proofs—requiring understanding of the publishing pipeline itself (arXiv structure, LaTeX environments, lemma dependency patterns).

But counterpoints:

• Dynamic anti-contamination is an engineering solution, not a conceptual breakthrough. It prevents contamination from published papers, but not authorial-style contamination: a mathematician whose decade of work is in training data has had their reasoning style encoded. A model proving their new lemma may be "mimicking their style," not "understanding math." This is contamination at the cognitive level—text-level deduplication is powerless against it.
• There's irony in using LLM-as-judge to verify LLM proofs. "Verifying is easier than proving" is true, but easier ≠ reliable. If two LLMs share correlated blind spots, cross-validation won't save you.

Even so, the post calls LemmaBench one of the most valuable math-evaluation works of 2026—not for dramatic results, but for its honesty. 10-15% is an uncomfortable number. It may be the true one.

Contributions and Limitations (from the paper)

| Item | Content | |------|---------| | Core contributions | (1) First dynamic math benchmark auto-extracting and self-containing research-level lemmas from arXiv; (2) full-context retrieval significantly beats vector retrieval (78.5% vs 49.4% self-containment); (3) GPT-5 is the highest-precision self-containment gatekeeper (few false positives); (4) top models achieve only 10-15% pass@1 on research-level lemma proving, revealing a qualitative gap between competition and research math; (5) historical versions are usable for training without affecting future evaluation, cutting the contamination chain | | Key limitations | LLM-as-judge reliability not fully human-verified; lemma difficulty distribution unreported; cultural dependence of "standard/classical" definitions undiscussed; dynamic-update infrastructure cost unquantified; cognitive-level homogenization contamination undefendable |

References: 1. Peyronnet et al., "LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics", arXiv:2602.24173v1, 2026. 2. Jain et al., "LiveCodeBench", 2024. 3. Patel et al., 2023; Alexander et al., 2026 (challenges in automatic arXiv formalization).