# LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics

arXiv: https://arxiv.org/abs/2602.24173 · HTML: https://mlsanity.com/paper/2602.24173/

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- Builds on 27 of its 49 references that are in the map.
- First posted on arXiv 27 Feb 2026.

## Builds on (most cited first, 27 of 27)

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code](https://mlsanity.com/paper/2403.07974/) (2024)
- [LongBench: A Bilingual, Multitask Benchmark for Long Context Understanding](https://mlsanity.com/paper/2308.14508/) (2023)
- [MathQA: Towards Interpretable Math Word Problem Solving with Operation-Based Formalisms](https://mlsanity.com/paper/1905.13319/) (2019)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models](https://mlsanity.com/paper/2410.07985/) (2024)
- [FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI](https://mlsanity.com/paper/2411.04872/) (2024)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Benchmarking Benchmark Leakage in Large Language Models](https://mlsanity.com/paper/2404.18824/) (2024)
- [Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models](https://mlsanity.com/paper/2503.21380/) (2025)
- [Magistral](https://mlsanity.com/paper/2506.10910/) (2025)
- [FIMO: A Challenge Formal Dataset for Automated Theorem Proving](https://mlsanity.com/paper/2309.04295/) (2023)
- [MathOdyssey: Benchmarking Mathematical Problem-Solving Skills in Large Language Models Using Odyssey Math Data](https://mlsanity.com/paper/2406.18321/) (2024)
- [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026)
- [PatternBoost: Constructions in Mathematics with a Little Help from AI](https://mlsanity.com/paper/2411.00566/) (2024)
- [Semi-Autonomous Mathematics Discovery with Gemini: A Case Study on the ErdHos Problems](https://mlsanity.com/paper/2601.22401/) (2026)
- [First Proof](https://mlsanity.com/paper/2602.05192/) (2026)
- [RealMath: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematics](https://mlsanity.com/paper/2505.12575/) (2025)
- [Global Lyapunov functions: a long-standing open problem in mathematics, with symbolic transformers](https://mlsanity.com/paper/2410.08304/) (2024)
- [Point Convergence of Nesterov's Accelerated Gradient Method: An AI-Assisted Proof](https://mlsanity.com/paper/2510.23513/) (2025)
- [A New Approach Towards Autoformalization](https://mlsanity.com/paper/2310.07957/) (2023)
- [Project Aletheia: Verifier-Guided Distillation of Backtracking for Small Language Models](https://mlsanity.com/paper/2601.14290/) (2026)
- [Semantic Search over 9 Million Mathematical Theorems](https://mlsanity.com/paper/2602.05216/) (2026)
- [EternalMath: A Living Benchmark of Frontier Mathematics that Evolves with Human Discovery](https://mlsanity.com/paper/2601.01400/) (2026)
- [Objective-Function Free Multi-Objective Optimization: Rate of Convergence and Performance of an Adagrad-like algorithm](https://mlsanity.com/paper/2602.05893/) (2026)

## Built on by (most cited first, 10 of 10)

- [Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs](https://mlsanity.com/paper/2605.00674/) (2026)
- [Matlas: A Semantic Search Engine for Mathematics](https://mlsanity.com/paper/2604.17484/) (2026)
- [Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness](https://mlsanity.com/paper/2605.10379/) (2026)
- [TCS-BENCH: Benchmarking State-of-the-Art Generative AI Theoretical Computer Science Research Ability](https://mlsanity.com/paper/2608.09538/) (2026)
- [Distilling LLM Feedback for Lean Theorem Proving](https://mlsanity.com/paper/2605.30861/) (2026)
- [GTBench: A Curriculum-Grounded Benchmark for Evaluating LLMs as Mathematical Research Assistants in Graph Theory](https://mlsanity.com/paper/2606.03144/) (2026)
- [The Ramanujan Challenge For AI](https://mlsanity.com/paper/2607.09721/) (2026)
- [Mathematical Discovery in the Wild: AI-Guided Proofs in Banach Space Theory](https://mlsanity.com/paper/2607.17388/) (2026)
- [TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science](https://mlsanity.com/paper/2609.35606/) (2026)
- [Large-scale factor analysis shows machine intelligence is only partially interpretable](https://mlsanity.com/paper/2609.36515/) (2026)

## Abstract (arXiv)

We present a new approach for benchmarking Large Language Model (LLM) capabilities on research-level mathematics. Existing benchmarks largely rely on static, hand-curated sets of contest or textbook-style problems as proxies for mathematical research. Instead, we establish an updatable benchmark evaluating models directly on the latest research results in mathematics. This consists of an automatic pipeline that extracts lemmas from arXiv and rewrites them into self-contained statements by making all assumptions and required definitions explicit. It results in a benchmark that can be updated regularly with new problems taken directly from human mathematical research, while previous instances can be used for training without compromising future evaluations. We benchmark current state-of-the-art LLMs, which obtain around 10-15% accuracy in theorem proving (pass@1) depending on the model, showing that there is currently a large margin of progression for LLMs to reach human-level proving capabilities in a research context.