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

> TL;DR: A team from ENS Rennes and École des Ponts/IP Paris built an automated "lemma harvesting machine" that extracts lemmas from the latest arXiv papers every week, automatically completes scattered definitions and assumptions, and turns them into self-contained standalone propositions. When top LLMs attempt them, pass@1 accuracy is only 10-15%. The leaderboard mythology built on competition math collapses in front of research-level mathematics.

| Item | Detail | |------|--------| | 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) | | 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 | Dynamically updated (refreshable weekly), contamination-resistant; historical versions usable for training without affecting future evaluation | | Coverage | Frontier branches across arXiv math categories: algebraic geometry, probability, analysis, combinatorics, etc. |

The Core Problem: Static Benchmarks Are a Slow Boil

The crisis in math reasoning benchmarks isn't new. GSM8K, MATH, AIME — these were once the touchstones of LLM mathematical ability. But as training data swelled to trillions of tokens, a specter has hovered: data contamination. Models may have seen benchmark problems, even solutions, during pretraining. Is a high test score real understanding, or memorization?

A subtler issue is distribution shift. Contest and textbook problems follow fixed patterns: complete conditions, standardized notation, unique answers. Real research papers embed lemmas mid-argument, with definitions scattered before them, references after, assumptions buried in footnotes. A lemma may require reading three earlier sections just to understand what it says. That is a different mental activity from "solving a word problem."

LemmaBench confronts both problems. The design philosophy is simple: if a model can prove a lemma mathematicians just wrote on arXiv today, it isn't reciting a question bank — because the bank hasn't been compiled yet.

The Pipeline: From Paper to Exam Question

Step 1: Harvest

The pipeline scrapes fresh preprints from arXiv math categories (math.AG, math.PR, etc.) and extracts lemma/theorem/proposition LaTeX environments via regular expressions. A second iteration added filtering: lemmas containing citations are discarded — those are restatements of known results, not new proofs.

Step 2: Complete

Research lemmas are rarely self-contained. A typical case: "By the preceding discussion, for functions f satisfying condition (3.2), we have..." — where condition (3.2) is on page 7 and "function f" is defined in Section 3.

Two completion strategies were tested:

• Full-context retrieval: feed everything before the lemma to an LLM and have it identify all missing definitions D and assumptions H making the lemma independently provable.
• Vector retrieval: give the LLM only the lemma, retrieve the most relevant passages via embeddings, then extract dependencies.

The result was decisive: full context crushes vector retrieval. Under GPT-5 full-context mode, 78.5% of lemmas were judged self-contained vs. only 49.4% with vector retrieval. The reason is simple — mathematical dependencies are often long-range, and embedding-based local similarity can't capture "a Section 3 definition implicitly used by a Section 9 lemma."

Step 3: Gatekeep

Completed lemmas go through an LLM-as-a-judge binary check: are the added definitions and assumptions sufficient for independence? Human mathematicians spot-checked: of lemmas judged "self-contained," 75.5-96.5% truly were (depending on extraction model and mode). GPT-5 was the most precise gatekeeper — conservative, with many false negatives but very few false positives — and became the default extractor.

Step 4: Examine

Self-contained lemmas become exam questions. Models receive the lemma statement plus completed definitions/assumptions and attempt proofs; an LLM judge evaluates proof validity, with human spot-checking of the judge. Crucially, historical versions can train models without affecting future evaluations — arXiv produces new papers weekly, severing the train-to-test leakage path.

What 10-15% Means

To be clear: this is not "models got 10% of math problems right." It is "models successfully proved 10-15% of cutting-edge research-level lemmas."

Results:

• GPT-5, Gemini 2.5 Pro / 3 Pro, Claude 4.5 Opus, DeepSeek-R — all in the 10-15% band
• No significant winner. Top models fail to differentiate on research-level math

Three readings:

1. Optimistic: models can prove some research lemmas. Not zero. Basic reasoning ability exists — just unstable and unsystematic. 2. Pessimistic: 10-15% means an 85-90% failure rate. A theorem requiring five lemma proofs has, under independent probabilities, less than a 10⁻⁵ success rate — effectively zero for real research. 3. Methodological: LemmaBench exposes a collapse in domain generalization. Models hit 90%+ on contest math because contest problems have fixed patterns, finite technique sets, and clear structure. Research math has open patterns, unknown techniques, structure that must be invented. The gap from contest to research is qualitative, not quantitative.

What Remains Unclear

• LLM-as-judge reliability ceiling: self-containment judgments were human-verified, but proof validity rests mainly on LLM judges with only partial human spot-checks. If judge error rates are non-uniform across proof styles (e.g., approving constructive proofs but misjudging contradiction arguments), the 10-15% figure carries systematic bias.
• Huge variance in lemma difficulty: arXiv lemmas range from trivial to requiring twenty pages of buildup. No difficulty distribution is reported; if the 10-15% comes mostly from trivial lemmas, true capability is lower.
• Cultural dependence of self-containment: what counts as "standard or classical" depends on subfield and reviewer background. The stability of LLM judges' criteria isn't discussed.
• Real update cadence: "weekly" refreshability is claimed, but the second iteration landed in February 2026, and infrastructure costs aren't quantified.
• Training/evaluation boundary: if a model trained on LemmaBench v1-v10 performs better on v11, is that genuine generalization or overfitting to LemmaBench's style? Finer ablations are needed.

My Take

LemmaBench's value isn't the "10-15%" number itself — it's the methodological correction. After two years of rising scores on GSM8K (95%+), MATH (90%+), and AIME (80%+), public discourse started discussing "AI mathematicians." LemmaBench is a bucket of cold water: those scores are real, but they measure the elementary stages of mathematical reasoning — pattern recognition, symbol manipulation, reproduction of known routines.

Dynamic evaluation isn't a new idea (LiveCodeBench, DyVal, NPHardEval all do it), but LemmaBench lands it in a domain that has traditionally resisted automation — research-level mathematical proofs — requiring not just technique but an understanding of the mathematical publishing process (arXiv structure, LaTeX environments, lemma dependency patterns).

Still, a cold shower in return: LemmaBench's dynamic contamination defense is an engineering fix, not a conceptual breakthrough. It blocks contamination from published papers but not author-style contamination. If mathematician A's decade of work has been trained on, the model may have learned A's mode of thinking; proving A's new lemma might be "imitating A's style" rather than "understanding mathematics." This is contamination at the cognitive level — homogenization — and LemmaBench is powerless against it.

There's also an irony: the paper uses LLM-as-judge to validate LLM proofs — the fox guarding the henhouse. "Evaluating proofs is easier than generating them" is true, but easier does not mean reliable. If two LLMs share correlated blind spots, cross-validation won't save you.

Even so, LemmaBench is among the most valuable math evaluation works of 2026 — not because its results are shocking, but because it is honest. 10-15% is an uncomfortable number, but it may be the true one.

Summary Table

| Item | Content | |------|---------| | Core contributions | (1) First dynamic math benchmark automatically extracting and self-containment-completing 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 most precise 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 contest and research math; (5) historical versions are trainable without affecting future evaluation, severing 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 costs unquantified; cognitive-level homogenization contamination undefended |

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).