LemmaBench: Live Research-Level Math Benchmark Drops Top LLMs to 10-15% Pass@1

Source: Peyronnet et al., "LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics", arXiv:2602.24173v1, February 27, 2026.

Key points

• Motivation. Existing math benchmarks (GSM8K, MATH, AIME) suffer from data contamination and distribution shift: contest-style problems have fixed patterns and complete information, while real research lemmas are embedded mid-argument, with definitions scattered across sections and assumptions hidden in footnotes. LemmaBench tests models on lemmas published on arXiv too recently to be in any training set.
• Four-step pipeline.
1. Harvesting: newest arXiv math preprints (math.AG, math.PR, etc.) are parsed with regex for lemma/theorem/proposition LaTeX environments; lemmas that merely restate known results (those containing citations) are filtered out. 2. Completion: two strategies restore self-containedness — full-context retrieval (the entire preceding paper is given to an LLM to extract missing definitions and assumptions) and vector retrieval (embedding-based passage search). Full-context wins decisively: 78.5% of lemmas judged self-contained with GPT-5 vs 49.4% for vector retrieval, because mathematical dependencies are often long-range and invisible to local similarity. 3. Gatekeeping: an LLM-as-judge performs a binary self-containment check. Human mathematicians verified that 75.5%-96.5% of lemmas judged self-contained truly were. GPT-5 was the most precise judge (conservative, few false positives) and is the default extractor. 4. Examination: models receive the lemma statement plus completed definitions/assumptions and attempt a proof; an LLM judge evaluates validity, with human spot-checking.
• Results. GPT-5, Gemini 2.5 Pro, Gemini 3 Pro, Claude 4.5 Opus, and DeepSeek-R all achieve roughly 10%-15% pass@1 on proving research-level lemmas, with no significant winner. Two interpretations: optimism — models can prove some genuine research lemmas, so basic reasoning exists; pessimism — an 85-90% failure rate compounds to near-zero success on multi-lemma research tasks (fewer than 10⁻⁵ if five lemmas must be proven independently). The gap from 90%+ on contest math is a qualitative collapse in domain generalization, not a quantitative shortfall.
• Anti-contamination design. Since arXiv continuously produces new papers, historical LemmaBench versions can be used for training without affecting future evaluations, severing the train-test leakage path.

Acknowledged limitations

• Proof-validity judging relies mainly on LLM judges, with only subset-level human verification; correlated misjudgment patterns could bias the 10-15% figure.
• Lemma difficulty variance is unreported; trivial lemmas may inflate scores.
• What counts as a "standard or classical" notion is culturally dependent on mathematical subfield.
• Infrastructure cost and true cadence of dynamic updates are unquantified.
• Author-style contamination (models encoding a mathematician's reasoning style from prior work) cannot be defended against — a deeper, cognitive-level form of homogenization that text-level anti-contamination does not address.

Editorial take

LemmaBench's value lies less in the headline number than in methodological correction: the 90%+ scores on GSM8K/MATH/AIME measure pattern recognition and reproduction of known techniques, which is only the early stage of mathematical reasoning. Dynamic evaluation is not new (LiveCodeBench, DyVal, NPHardEval), but LemmaBench lands it in a domain traditionally very hard to automate — research-level proof — requiring understanding of arXiv structure and LaTeX lemma-dependency patterns. Despite its limitations, it is an unusually honest measurement of where frontier LLMs actually stand in mathematics.

Reference: Peyronnet, Gloeckle, Hayat, "LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics", arXiv:2602.24173v1, 2026.