LemmaBench: A Live, Research-Level Benchmark That Turns Benchmark Champions Back Into Novices

> TL;DR: A team from ENS Rennes and IP Paris built a "mathematical lemma harvester" — a pipeline that extracts lemmas weekly from the latest arXiv papers, automatically completes scattered definitions and assumptions, and turns them into self-contained standalone propositions. When top LLMs attempt to prove them, pass@1 accuracy is just 10-15%. Competition-benchmark glory 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 judgment (LLM-as-judge + human validation) → theorem proof 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: ~10-15%, depending on model | | Dataset features | Dynamically updated (can refresh weekly), contamination-resistant, historical versions usable for training without affecting future evaluations | | Coverage | Frontier branches of arXiv math categories: algebraic geometry, probability, analysis, combinatorics, etc. |

The Core Problem: Static Benchmarks Are a Slow Boil

The crisis in mathematical reasoning benchmarks is not new. GSM8K, MATH, AIME — these were once the touchstones of LLM mathematical ability. But as training data swelled to trillions of tokens, one specter has always loomed: data contamination. Models may have seen GSM8K problems, even solutions, during pretraining. Is a high test score genuine understanding, or memorization?

A subtler issue is distribution shift. Competition and textbook problems follow fixed patterns: complete conditions, standardized notation, unique answers. In real research papers, a lemma often sits mid-argument, with definitions scattered before it, citations after, and assumptions buried in footnotes. Understanding a lemma may require reading the paper's first three sections. This is a fundamentally different mental activity from solving an application problem.

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

The Pipeline: From Papers to Exam Questions

Step 1: Harvest

The pipeline scrapes the latest preprints from arXiv math categories (math.AG, math.PR, etc.) and uses regular expressions to extract LaTeX environments for lemmas, theorems, and propositions. A second iteration added filtering: lemmas containing citations are discarded — those are restatements of known results, not new proofs.

The harvest is plentiful, but most lemmas can't be used directly.

Step 2: Complete

Lemmas in math papers are rarely self-contained. Typical scenario: "From the preceding discussion, for functions f satisfying condition (3.2), we have..." — condition (3.2) is on page 7, the definition of f is in Section 3, the lemma is on page 9.

Two completion strategies were designed:

Full-context retrieval: Feed the entire paper preceding the lemma to an LLM, asking it to find all missing definitions D and assumptions H that make the lemma an independently provable statement under D and H.

Vector retrieval: Give the LLM only the lemma, use embeddings to retrieve the most relevant passages from the paper, then extract dependencies from those.

The result was decisive: full-context crushed vector retrieval. 78.5% of lemmas were judged self-contained under GPT-5 full-context mode, versus only 49.4% for vector retrieval. The reason is simple — mathematical dependencies are often long-range; embedding-based local similarity cannot capture structures like "a definition in Section 3 implicitly used by a lemma on page 9."

Step 3: Gatekeep

Completed lemmas go to an LLM-as-judge for a second check: are the added definitions and assumptions sufficient for the lemma to stand alone? Output is a binary verdict plus reasoning.

Human mathematicians spot-checked this gatekeeping. Result: of lemmas judged "self-contained" by the LLM, 75.5-96.5% were genuinely self-contained (depending on extraction model and mode). GPT-5 was the highest-precision gatekeeper — conservative, with many false negatives but very few false positives.

GPT-5 was chosen as the default extractor.

Step 4: Examine

Self-contained lemmas become exam questions. Models receive the lemma statement plus completed definitions/assumptions and attempt a proof. An LLM-as-judge evaluates proof validity, with human mathematicians spot-checking subsets to score judge reliability.

Key design: historical versions of LemmaBench can be used for training without affecting future evaluations — because arXiv produces new papers every week. This severs the "training set leaking into test set" pipeline.

The Results: What 10-15% Means

To be clear: this isn't "the model got 10% of math problems right." It's "the model successfully proved 10-15% of the latest research-level lemmas."

Research-level lemmas are auxiliary results mathematicians invent to advance frontier theorems. They typically require: understanding a non-standard definition, recognizing hidden structural patterns, constructing a non-trivial auxiliary object, or combining known techniques in novel ways. This is a different universe from "Xiao Ming has 5 apples."

Performance across models:

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

Optimistic: models can genuinely prove some research-level lemmas. Not zero. Basic reasoning ability exists — just unstable and unsystematic.

Pessimistic: 10-15% means an 85-90% failure rate. A theorem requiring five lemma proofs, computed on independent probabilities, has a success rate below 10⁻⁵. In practice, that's zero.

Methodological: LemmaBench exposes a collapse in domain generalization. Models hit 90%+ on competition math because competition problems have fixed patterns, a finite technique set, and explicit problem structure. Research math has open-ended patterns, unknown techniques, and structures that must be invented. The gap from competition to research is qualitative, not quantitative.

Honest Unknowns

The reliability ceiling of LLM-as-judge: self-containment judgments were human-validated, but proof-validity verification relies mainly on LLM judges; humans only spot-checked subsets. If LLM judges misjudge complex proofs non-uniformly — e.g., accepting constructive proofs readily but misjudging proof by contradiction — the 10-15% figure carries systematic bias.

Extreme variance in lemma difficulty: arXiv lemmas range from trivial ("immediate from the definition") to formidable (requiring twenty pages of setup). The paper doesn't report the difficulty distribution. If the 10-15% comes mostly from trivial lemmas, actual capability is lower.

Cultural dependence of self-containment judgments: what counts as "standard or classical" without further definition depends on mathematical subfield and reviewer background. A concept an algebraic geometer considers "standard" may be unknown to a number theorist. Is the LLM judge's standard stable? The paper doesn't discuss it.

Real update frequency: the paper says "can update weekly," but the second iteration was February 2026. How long between launch and iteration two? Is the infrastructure cost of dynamic updates (scraping, LLM calls, human spot-checks) sustainable? Unstated.

Training-evaluation boundary: historical versions can be used for training. But 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 course correction.

Over the past two years, LLM mathematical ability has been inflated by a string of high scores: GSM8K 95%+, MATH 90%+, AIME 80%+. The discourse started discussing "AI mathematicians" and "AI-assisted proofs." LemmaBench is a bucket of cold water: those scores are real, but they measure the early stages of mathematical reasoning — pattern recognition, symbol manipulation, reproduction of known routines. Research-level mathematics requires something else.

Deeper, LemmaBench addresses a meta-question in AI evaluation: when benchmarks are contaminated, the entire edifice of evaluation collapses. Dynamic evaluation isn't new (LiveCodeBench, DyVal, NPHardEval all do it), but LemmaBench lands it in a domain historically extremely hard to automate — research-level mathematical proofs. That requires not just technique but an understanding of the mathematical publishing process (arXiv structure, LaTeX environments, lemma dependency patterns).

But let me splash some cold water back.

LemmaBench's "dynamic anti-contamination" is an engineering solution, not a conceptual breakthrough. It guards against contamination by published papers — the model hasn't seen the paper because it was just released. It cannot guard against contamination by author style. If mathematician A's decade of work has been in the training data, the model may have learned A's mode of thinking. A's new paper isn't in the training set, but A's reasoning style is already encoded. When the model proves A's new lemma, it may be "imitating A's style" rather than "understanding mathematics."

This is deeper contamination — not textual duplication but cognitive-level homogenization. LemmaBench is powerless against it.

There's also an irony: the paper uses LLM-as-judge to validate LLM proofs. That's the fox guarding the henhouse. "Evaluating proofs is easier than generating them" — true, but "easier" isn't "reliable." If two LLMs' misjudgment patterns correlate (both blind to the same errors), cross-validation won't save you.

Even so, LemmaBench is among the most valuable mathematical evaluation works I've seen in 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.

> | Item | Details | > |------|---------| > | Core contributions | (1) First dynamic math benchmark that automatically extracts research-level lemmas from arXiv and makes them self-contained; (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 (very 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 trainable without affecting future evaluations, 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 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 (inspiration for dynamic evaluation). 3. Patel et al., 2023; Alexander et al., 2026 (challenges of automatic arXiv formalization).